- Efficient integer arithmetic in Coq.
- Translating terms in first-order logic to increase automation in Coq
- Integrating the Metis automatic theorem prover into the Coq proof assistant
- Data-Mining and Refactoring for arithmetic in Coq
- Formalisation of linear algebra
- Formal proof of a theorem about biological models

Yves Bertot Last modified: Tue March 5 14:04:37 MEST 2013