Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
The Coquelicot library
The Coquelicot library - The Coquelicot library

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
Software & patents
The C++ Bulk Synchronous Parallelism Library

A prototype to automate semantic mappings between taxonomies

Procédé pour l’extinction de routeurs dans un réseau de communications et routeur mettant en œuvre ce procédé