Rocqet proof language

An encoding of linear logic in Coq with minimal Sokoban and blocks world examples

Coq library for handling names

Formalization of Axiomatic Set Theory in Coq

translations of a lambda abstraction to combinations of operators

Implementation of sprintf for Coq

Formal Semantics for Why3

Formalization of Typed Assembly Language (TAL) in Coq

A Hello World program in Coq.

Towards Optic-Based Algebraic Theories: the Case of Lenses

Calculus of Constructions

Haskell implementation and Coq proof for an implicit polymorphic gradual type system.

Mechanized Theory of Event Structures

Formalization of some elementary mathematical theories in Coq

Writeup that goes along with this:

Linearizability Hoare Logic

Coq proof for elaborating row polymorphism and bounded polymorphism into disjoint polymorphism.

Large category of modules over monads on top of UniMaths and Display category

Attempt to prove semantic preservation (forward simulation) for a simple compiler.

Mechanized proofs and example programs for the paper Type Inference Logics, published at OOPSLA24.

Work based on http://www-sop.inria.fr/marelle/GeometricAlgebra/

Formalisation of the linear lambda calculus in Coq

Verified SSA-Based Register Assignment

Formalization of Linear Logic and Related Programming Languages Metatheory

Proofs of correctness for Scallion (https://github.com/epfl-lara/scallion)

A Coq implementation of a nanopass compiler, using "Meta-Theory à la Carte" techniques