Coquelicot

2011-2014 research project
  • 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.