A (formalised) general definition of type theories

A framework for implementing and certifying impure computations in Coq

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

Bidirectional programming in Haskell with monadic profunctors

Total Parser Combinators in Coq [maintainer=@womeier]

Implementation of Nuprl's type theory in Coq

A Certified Interpreter for ML with Structural Polymorphism

Replib: generic programming & Unbound: generic treatment of binders

Repository where I'll collect some demos of proof assistants that I show to various people in order to spread the magic

GoNative project: formal machines models in Coq

IO for Gallina

VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations

Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]

MPRI-2.4 Dependently-typed Functional Programming

Finite sets and maps for Coq with extensional equality

Coq library for working with de Bruijn indices [maintainer=@KevOrr]

Formally verified operator language and rewriting engine for high-performance computing

Bedrock Bit Vector Library

This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides bot…

A certified semantics for relational programming workout.

Building A Correct-By-Construction Proof Checkers For Type Theories

Graded Dependent Type systems

Verified and Efficient Matching of Regular Expressions with Lookaround

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

Based on paper by Greg Morrisett , TAL-0 is the design of a RISC-style typed assembly language which focuses on control-flow safety.

A Model of Relationally Parametric System F in Coq