LOGICAL : Logic and computing (project-team)

About the project : Project-Team site Activity report Videos and photos Research reports Theses Theme : Sym Symbolic systems Saclay - Île-de-France research center

LOGICAL has been dissolved on 12/31/2007
It has been replaced by TYPICAL

Project-Team Presentation

Joint project-team with LRI (CNRS and University of Paris-Sud) and LIX (CNRS and Ecole Polytechnique).

The Logical 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 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

• The European working groupTypes.
• The joint European research projectMOWGLI on development and management of mathematical documents on the Web.
• Averroes: Analysis and Verification for the Reliability Of Embedded Systems
• Geccoo: Certified code generation for object oriented applications
• Modulogic: creation of a tool for certified software generation.

Scientific leader

Gilles DOWEK
+33 1 69 33 43 06
Gilles.Dowek@inria.fr
Secretary : +33 1 69 33 34 85

Team Address

LIX
Ecole Polytechnique
91129 Palaiseau Cedex