Current
- Computing efficiently within Coq.
- Formalizing Z-homology.
- Exploring the consequences of the homotopic point of view and of the univalence axiom on type theory.
Past
- Formalization of real algebraics numbers in Ssreflect
- Quantifier Elimination in Real Closed Fields in Ssreflect
- Quantifier Elimination in Algebraically Closed Fields in Ssreflect
- Multinomials in Ssreflect
- Quotient Types in Ssreflect
- Reification using Canonical Structure in Coq and Ssreflect