Wiki Agenda Contact Version française

Formalization and Certification of Languages, Tools and Systems


Development of Coq libraries

Higher-order strongly typed programming languages such as Objective Caml help improving the quality of software development. Static typing automatically detects possible execution errors. Higher-order functions, polymorphism, modules and functors are powerful tools for the development of generic reusable libraries. Our general goal is to enrich such a software environment with a language of annotations as well as libraries for data types, abstract notions and associated theorems which can express logical properties of programs and ease the possibility to automatically and interactively develop proofs of correctness of the programs. In the past, we made contributions to the Coq proof assistant by adding features for improving the development of formally proved functional programs. A first contribution is a new method to extract Ocaml modular code from Coq proofs (P. Letouzey's PhD thesis). This extraction mechanism is an original feature for the Coq system, and has been used by several teams around the world in order to get efficient certified code. Another contribution (M. Sozeau's PhD thesis) is an extension of the Coq input language for building programs with strong specifications by writing only the computational part and generating proof obligations separately (which are usually solved by tactics) and also a mechanism generalizing Type Classes à la Haskell which gives overloading in programs and proofs and facilitates the development of generic tactics.

Our current activities mainly focus on using the capability of the Coq system to model both computation and deduction in order to explore different classes of applications. These examples involve the development of large reusable Coq libraries and suggest domain-specific specification and proof strategies.

Randomized algorithms

We proposed a method for modeling probabilistic programs in Coq. The method is based on a monadic interpretation of probabilistic programs as probability measures. It is available as a Coq library ALEA. This library has been used in an environment Certicrypt for the interactive development of formal proofs for computational cryptography.

Floating-point programs

A high-level of guarantee on floating-point computations is obtained by formal proofs in Coq. We maintain and develop large Coq libraries (such as Flocq and PFF) for floating-point arithmetic: core definitions, axiomatic and computational rounding operations, high-level properties. They provide a framework for developers to formally certify numerical applications. More details can be found here.

Real analysis

We have worked on easing proofs of differentiability and integrability in Coq. The use case was the existence of a solution to the wave equation thanks to D'Alembert's formula; the goal was to automate the process as much as possible. Our approach is based on the pervasive use of total functions. We aim at creating a modern formalization of the real numbers in Coq, with a focus on practicality. This is sorely needed to ease the verification of numerical applications, especially those involving advanced mathematics.

Certification of tools

alt-ergo as a reflexive tactic in Coq Certifying the result of tools for analysing programs is a good challenge in the domain of proofs of higher-order functional programs.

The proof assistant Coq can be used to certify the result of automated deduction tools. We developed a certified version of the kernel of the alt-ergo theorem prover (S. Lescuyer PhD thesis). We are also developing a library Coccinelle for reasoning on termination of term rewriting systems. These results are described here.

We are also currently developing a certified version the Frama-C/Jessie/Why verification chain.

Contribution to functional programming

We develop several advanced tools in Objective Caml, some specific to our research objectives but some of a more general purpose which we distribute as open-source libraries.


Sylvie Boldo, Evelyne Contejean, Jean-Christophe Filliâtre, Paolo Herms, Catherine Lelay, Claude Marché, Guillaume Melquiond, Christine Paulin-Mohring, Xavier Urbain.

Former contributors

Romain Bardou, François Bobot, Johannes Kanig, Stéphane Lescuyer, Pierre Letouzey, Matthieu Sozeau.

Software developments

Coq libraries

Ocaml libraries and general tools

Related Grants

Main Publications

  1. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. In Proceedings of the Second International Conference on Certified Programs and Proofs, Kyoto, Japan, December 2012. [ bib | full paper on HAL ]
  2. Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier Pons, and Xavier Urbain. A3PAT, an Approach for Certified Automated Termination Proofs. In Partial Evaluation and Program Manipulation, Madrid, Spain, january 2010. ACM Press.
  3. Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568-589, 2009. [PDF]
  4. Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant. In John Rushby and N. Shankar, editors, AFM07 (Automated Formal Methods). ACM Press, 2007. [PDF]
  5. Matthieu Sozeau. Un environnement pour la programmation avec types dépendants. Thèse de doctorat, Université Paris-Sud, December 2008. [bib]

Other Related Publications

  1. Christine Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. In Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin, editors, From Semantics to Computer Science: Essays in Honor of Gilles Kahn. Cambridge University Press, 2009. [PDF]