My contributions to the development of the Coq proof assistant are:
- A reduction engine which reuses the OCaml native compiler, useful for intensive computations inside proofs (with Benjamin Grégoire and Mathieu Boespflug).
- A branch called native-coq which adds primitive machine integers and persistent arrays (with Benjamin Grégoire).
- A fix for the guard condition for fixpoints and cofixpoints, restoring the compatibility of Coq's logic with extensionality axioms (with Bruno Barras).
- Various bug fixes and maintenance tasks.
I'm also one of the authors of:
- CoqEAL, a Coq library for effective algebra. It includes a refinement framework, which makes it easier to separate proof-oriented data structures from computation-oriented ones, with automatic transport of proofs between them.
- QuickChick, a Coq plug-in for property-based random testing with verified generators.
- A Coq formalization of micro-policies, which are hardware-assisted security monitors.