Pangolin, a functional language to prove pure higher-order programs. The current implementation is a prototype. I am working on a realistic implementation currently.
Pangoline, a theorem prover for higher-order logic. It is based on an encoding of polymorphic higher-order logic theories into polymorphic first-order logic theories. This will be the back-end of the new version of Pangolin. Joint work with Johannes Kanig.
Menhir, a LR(1) parser generator. Joint work with François Pottier.
Mini, a constraint-based type inference engine for ML. Here is an online documentation of the code. Here is an online prototype. Joint work with François Pottier and Didier Rémy.