152 Open source projects that are alternatives of or similar to Verlang

Formal Reasoning About Programs

An introductory course to Homotopy Type Theory

Combinatorial species in HoTT

An axiom-free formalization of category theory in Coq for personal study and practical work

A proof of Abel-Ruffini theorem.

Coq executable semantics and resource verifier

Mathematical Components

Bidirectional programming in Haskell with monadic profunctors

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Automation for de Bruijn syntax and substitution in Coq

KCoFI Pudding: The formal proofs for the KCoFI system

Ltac2 tutorial

Cosette is an automated SQL solver.

Coq plugin for parametricity [[email protected]]

This repo is the new home of Proof General

Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.

Tricks you wish the Coq manual told you

A framework for implementing and certifying impure computations in Coq

A gently curated list of companies using verification formal methods in industry

CoqPIE (an IDE for the Coq theorem prover + PEDANTIC)

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

Implementation of sprintf for Coq

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Coq proofs of exercises in Pierce's book

Mtac in Agda

sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

The CompCert formally-verified C compiler

《软件基础》中译版 Software Foundations Chinese Translation

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

A framework for formally verifying distributed systems implementations in Coq

Porn browser formally-verified in Coq

A port of Coq to Javascript -- Run Coq in your Browser

Formalisation of the linear lambda calculus in Coq

Cryptographic Primitive Code Generation by Fiat

Implementation of Nuprl's type theory in Coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

Coq code accompanying several articles on semantics of functional programming languages

A Coq IDE build on top of Proof General's Coq mode

The Penn Locally Nameless Metatheory Library

Convert Haskell source code to Coq source code

An introductory tutorial for the Coq proof assistant.

Verified Software Toolchain

Homotopy type theory

IO for Gallina

Formalization of C++ for verification purposes.

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

A Certified Interpreter for ML with Structural Polymorphism

Formal verification of OCaml programs

Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors

Finite sets, finite maps, multisets and generic sets

Verified vector clocks, with Coq!

A Coq library for extensional finite sets and comprehension

Formal specification and verification of hardware, especially for security and privacy.

A blog about Coq

Total Parser Combinators in Coq

A Hello World program in Coq.

Certified Relational to Imperative