Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

INRIA-Futurs

The LogiCal project of INRIA-Rocquencourt has moved to INRIA-Futurs at the École polytechnique. The main topic is the development of proof systems, in particular the Coq system, but it is also involved in the development of formal libraries and challenging formal proofs and in the study of logical formalisms such as type theory, inductive types, sequent calculus and deduction modulo.

The senior members of the group are

• Gilles Dowek, contact person
• Bruno Barras
• Hugo Herbelin
• Jean-Pierre Jouannaud
• Dale Miller
• Benjamin Werner

The group has a strong cooperation with the Paris Sud group. We have strong cooperation with two industrial subsites : Trusted Logic and France Telecom. We have exchanged doctoral and post-doctoral students with Chalmers, Warsaw, Cambridge, Sophia. We have frequent cooperation with most of the sites of the proposal.

Members of the group have been teaching in the various Types summer schools.

INRIA-Futurs homepage