TYPICAL Research team

Types, Logic and computing

Team presentation

The Typical project-team 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-team federates and coordinates the development of the proof-system Coq which allows the interactive specification and construction of formal proofs. The language of Coq 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.

The TypiCal project-team stems from the Coq project, which was joint 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. This was followed by the LogiCal project-team which was a common project with the Laboratoire de Recherche en Informatique (URA CNRS 410) from University Paris Sud until december 2007.

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 mathematical libraries.

International and industrial relations

Research teams of the same theme :

Inria Headquarters and research centres

Direct links

Social