The ProVal team was stopped at the end of August 2012, and reborn into a new team
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Computer-Assisted Proof and Functional Programming
Higher-order strongly typed programming languages such
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
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.
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.
Floating-point programsA high-level of guarantee on floating-point computations is obtained by formal proofs in Coq. We maintain and develop large Coq libraries for floating-point arithmetic: core definitions, axiomatic and computational rounding operations, high-level properties. It provides a framework for developers to formally certify numerical applications. A new such library is described Flocq is under construction. These results are described here.
Certification of toolsCertifying 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 programmingWe 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.
- Bibtex2html is a generator of HTML pages of bibliographic references distributed as open source since 1997. We estimate that between 10000 and 100000 web pages have been generated using Bibtex2html.
- We designed and implemented Ocamlgraph, a highly generic graph library for the programming language Ocaml. This library features a large set of graph data structures - directed or undirected, with or without labels on vertices and edges, as persistent or mutable data structures, etc. - and a large set of graph algorithms. Algorithms are written independently from graph data structures, which allows combining user data structure (resp. algorithm) with Ocamlgraph algorithm (resp. data structure).
- We designed Mlpost an API to program metapost figures with Ocaml.
- We supervised the design of Ocamlviz funded by Jane Street Capital within the framework of Jane Street Summer Project. The key idea of Ocamlviz is the ability to instrument an existing code, in real time, with lightweight monitoring annotations. Ocamlviz can also be used as a debugging tool.
- We proposed efficient functional implementations of data-structures such as persistent arrays and ropes (see here for more information).
PeopleRomain Bardou, François Bobot, Sylvie Boldo, Evelyne Contejean, Jean-Christophe Filliâtre, Paolo Herms Claude Marché Guillaume Melquiond, Christine Paulin-Mohring Xavier Urbain
Former contributorsJohannes Kanig, Stéphane Lescuyer, Pierre Letouzey, Matthieu Sozeau
- ALEA : a Coq library for reasoning on randomized algorithms
- Coccinelle: a Coq library for term rewriting systems
- Flocq: a Coq library for formal proofs on floating point numbers
Ocaml libraries and general tools
- bibtex2html: generation of HTML pages from bibliographies
- Ocamlgraph: Objective Caml library for graphs
- Mlpost: Ocaml front-end for producing figures
Series of verified programs
- ANR Project SCALP
- Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in Coq. Science of Computer Programming, 74(8):568-589, 2009. [PDF]
- 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]
- É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.
- Pierre Letouzey. Programmation fonctionnelle certifiée: l'extraction de programmes dans l'assistant Coq. Thèse de doctorat, Université Paris-Sud, July 2004. [.ps.gz]
- Matthieu Sozeau. Un environnement pour la programmation avec types dépendants. Thèse de doctorat, Université Paris-Sud, December 2008. [bib]