A compiler for a simple language using llvm

Lean4: Total parser combinator library with do notation

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

Recursive first-class modules prototype for master's thesis

Open records implemented using map over universal type

Play and Enjoy the History of Microsoft Flight Simulator

Terrain rendering algorithm in less than 20 lines of code

An experimental mutual induction tactic for Lean 4.

A typechecker and lazy interpreter for System U

Parser for a mini ML-like language (re2ocaml + Menhir)

Apple corecrypto

Better Type Theory for Idris

A kind synthetic Euclidean Geometry proof assistant

being a programming language for sequential circuits

A common exchange format for logical systems expressed in terms of inference rules.

🤖 Just a command runner

Pure Haskell SAT solver

a structural diff that understands syntax 🟥🟩

Logical relations proof in Agda

Snapshotable WebAssembly interpreter from scratch. Includes a time travel debugger

Official Website

OCaml with macros

Strymonas for OCaml with modular macros

An experiment to see what interpretation into (pre)sheaves categories look like

A reactive notebook for Python — run reproducible experiments, query with SQL, execute as a script, deploy as an app, and version with git. Stored as pure Python. All in a modern, AI-native editor.

OCaml hash-consing library