xmonad in Coq

toy implementation of Hindley-Milner type system that prints out inference steps

A OCaml generator for well-typed terms (that use their arguments).

A Rocq version of the miniF2F dataset

Composable monadic STM for C++ on Free monads

Artifact for OSDI '23 Paper "Spoq: Scaling Machine-Checkable Systems Verification in Coq".

For Jar artifacts

Trying to do existential proofs with coinductive values.

Implement OCaml APIs in Coq

A fuelled self-reducer for System T, embedded in Idris 2

A typechecker and compiler for a higher-order language of regular types.

A Deductive Verification Tool for OCaml Programs

A port of Doom (1993) that runs inside a PDF file

A Lean implementation of Interaction Trees

Verified Multiplicative Weights Update

A Coq/Mathematical Components library for mechanism design

Lean 4 kernel / 'external checker' written in Lean 4

Write your own virtual machine for the LC-3 computer!

Separation Logic Proofs in Lean

A Verified Implementation of Dijkstra's Algorithm

An automated deductive program verifier based on concurrent separation logic

Giving types to jq

A modern supercompiler for call-by-value functional languages

Seer - a gui frontend to gdb

A recreation of the classic Visual Basic 6 IDE and language in C# with Avalonia

A reflection-based proof tactic for lattices in Coq

Demo for dependent types + runtime code generation