Fran├žais Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software The Coquelicot library
The Coquelicot library - The Coquelicot library
Date of the last release: 07 September 2017

Person in charge : BOLDO Sylvie

Coquelicot is a user-friendly Coq library for real analysist.
An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals, two-dimensional differentiability, asymptotic behaviors. It also offers some automations for performing differentiability proofs. Moreover, Coquelicot is a conservative extension of Coq's standard library and we provide correspondence theorems between the two libraries. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation

More information:


Research activities
  Formalisation of (Specification and Programming) Languages in Proof Assistants

  BOLDO Sylvie
  MELQUIOND Guillaume
  LELAY Catherine

  Verification of Algorithms, Languages and Systems

Joint Inria project team
Software & patents

Deep Neural Architectures for DNA