A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

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

A work-in-progress language and compiler for verified low-level programming

Randomized Property-Based Testing Plugin for Coq

Programming Language for Smart Legal Contracts

A mechanisation of Wasm in Rocq

Writeup that goes along with this:

A Coq to Cedille compiler written in Coq

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

Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2020

linear algebra done right in coq

Strong Normalization for Simply-Typed Lambda-Calculus with de Bruijn indices in Coq

System F in Coq

Learning Coq via Software Foundations