Current
- Exploring the consequences of the homotopic point of view and of the univalence axiom on type theory.
- Computing efficiently within Coq.
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
This page was last updated at
2013-01-23 18:00:18 +0100