Contact
Sylvie Boldo is coordinator of this project.E-mail:Sylvie.Boldo@inria.fr
Address:
Sylvie Boldo
PCRI - Bâtiment 650
Université Paris-Sud
91405 Orsay Cedex
FRANCE
- 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 using the corresponding ssreflect library.