Types, logic and calculus

Research Topics

The goal of the research conducted in our project is to construct proof processing systems, i.e. systems that are able to process mathematical knowledge. Such a system can verify that a proof does not contain any error, it can help the users to construct proofs in an interactive way, search proofs automatically, store proofs in bases, transmit them on the net, ...

Using a computerized system to process mathematical proofs permits to reach a high degree of certainty, that a proof does not contain any error. This can be applied, in particular, to proofs justifying the correcteness of programs and hardware. This is of prime interest for applications where a bug may jeopardize human life, health or environment, or when large amounts of money are involved : medical applications, transportations, telecommunications, e-business, distributed applications, ... Using a proof processing system permits also to build large proofs, for instance proofs involving polynomials formed with several hundreds of terms. At last, this participates to the quest of a new form of rigour in mathematical writing : the point where nothing is left implicit and where the reader can be replaced by a program.

The main line of research in our work is the development of the system Coq. This system has a large community of industrial and academic users. However, we believe that the development of a system cannot be separated from a more applied research on the uses of this system in particular domains (such as geometry, proofs of imperative or object-oriented programs, proofs of protocols, ...) and a more fundamental research on the formalization of mathematics (on the representation of proofs, on the integration of a programming language in a mathematical formalism, on the notion of bound variable, ...). This research involves two key notions: that of logical reasonning and that of computation. These two notions give its name to the project TypiCal (Types et Calcul).