Computer Code

I'm currently a member of Deducteam at Inria Paris Saclay. I'm a former member of the ALEXANDRIA project led by Lawrence Paulson, of the Programming, Logic and Semantics Group, of the Automated Reasoning Group and of The Cambridge Logical Structures Hub at the University of Cambridge.  

• hol2dk: exporting HOL-Light proofs to Dedukti, Lambdapi and Coq

• Some number theory in Isabelle/HOL (jww Manuel Eberl, Wenda Li and Larry Paulson)

• The Silicon Geometer project 

• Some differential geometry in the Lean theorem prover (with Nicolò Cavalleri).

• A pilot study where we formalized (with Michael R. Douglas) Lie groups in the proof assistant Isabelle.

• Check our library of quantum computing certified with the proof assistant Isabelle.

• UniLab, formalized mathematics based on the UniMath library implementing the ideas of the Univalent Foundations, 2017 (using the proof assistant Coq).