Fouine
A faithful interpreter for a substantial subset of OCaml, written in OCaml.
Projects
This page lists selected academic and research-oriented projects.
Idris Frex
I contributed to the Idris Frex project, a library which offers a new approach to synthesising algebraic proofs in dependently-typed programming languages, based on free extensions from universal algebra.
Pieuvre
A proof assistant based on the Calculus of Inductive Constructions, inspired by Rocq and written in OCaml.
VeriSLO
A tool for streamlining Iris proofs of OCaml programs.