Projects

This page lists selected academic and research-oriented projects.

Fouine

A faithful interpreter for a substantial subset of OCaml, written in OCaml.

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.