- Published article at JFLA 2012.
- Published article at CPP 2012 about a user-friendly approach to integrals and derivatives in Coq.
- Accepted article at the 2013 Coq workshop about a new formalization of Power Series: browse it.
- Accepted journal article: Coquelicot: A User-Friendly Library of Real Analysis for Coq in Mathematics in Computer Science, 9(1):41-62, 2015. [DOI | http ]
- Accepted journal article: Formalization of Real Analysis: A Survey of Proof Assistants and Libraries in Mathematical Structures in Computer Science, 2015. [DOI | http ]
- All those works (except the last one being a survey) are part of the freely available Coquelicot library:
click here to download the latest version or browse the library.
This library compiles with Coq 8.4 and 8.5 using the corresponding ssreflect library.