Sites Inria

Version française

COQ Research team

Formal Specifications and Program Validation

  • Leader : Christine Paulin-mohring
  • Research center(s) : CRI de Paris
  • Field : Software engineering and symbolic computing
  • Theme : Semantics and Programming

Team presentation

The Coq project aims to elaborate a language and environment for the development of formal proofs. This environment is dedicated to the development and certification of zero-default programs in safety-critical software.

The project develops an environment (Coq) for interactively elaborating specifications and proofs. Its language is based on Type Theory: the functions can be represented by algorithms, predicates can be inductively defined by a set of clauses, proofs are considered as objects in the language.

Coq was a project common with the Laboratoire de l'Informatique du Parallélisme (URA CNRS 1398) of the École Normale Supérieure de Lyon from January 1994 to September 1997. It should soon become a common project with the Laboratoire de Recherche en Informatique (URA CNRS 410) from University Paris Sud.

Research themes

  • High-level concepts for proof languages: modules, subtyping, definitions by patterns, infinite structures.
  • Internal representation of proof terms for an efficient implementation of reduction and proof construction.
  • Development of mathematical proofs and certified programs (especially the proof of the Coq kernel itself).

International and industrial relations

  • Participation in the Esprit LTR "Types" working group.
  • Participation in the Dassault-INRIA engineering action on proof technology.
  • Collaboration with the Bull Research Center on protocol proofs within the Dyade GIE.
  • Collaboration with the Cnet in Lannion on proof technology.
  • Participation in cooperative action CFC-Calcul Formel Certifie.

Keywords: Typing Logic Lambda-calculus Functional language Formal computing Formal specifications Automated deduction Program synthesis Program validation Secure network protocols