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: