Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

INRIA-Sophia

The large and active group at INRIA Sophia-Antipolis has been part of all previous EU funded TYPES projects. The group has made many large formal proof developments using the Coq proof tool, including formalisation of programming language semantics (e.g. Java, in collaboration with other TYPES teams in Paris Sud and Munich), and formalization of mathematics (e.g. formalization of rational numbers, and of Gröbner bases, in collaboration with Nijmegen and Chalmers). INRIA Sophia and INRIA Rocquencourt participate in the INRIA action "Concert: Certified Compiler"quot;; this is a broad project on the certified implementation of compilers for "real" programming languages such as C. Members of the team have done much foundational work on induction reasoning with higher-order specifications. The team has also been active in building interfaces for proof tools. Yves Bertot (with Pierre Castéran of University of Bordeaux) has written a textbook about using the Coq proof system for practical applications.

The senior members are

• Joëlle Despeyroux, contact person
• Gilles Barthe
• Yves Bertot
• Marieke Huisman
• Luigi Liquori
• Loïc Pottier
• Laurence Rideau
• Laurent Théry

The site plans to contribute to the following objectives of the current proposal.

Correctness of Computer Systems

The group is interested in programming with dependent types, and also plans to work on some challenge for practical formalization, such as computer arithmetic.

Foundational Research

The group is actively involved in work on inductive definitions, subtyping, rewriting, termination, logical frameworks and type isomorphism.

Formal mathematics

The group will do case studies, and particularly participate in building a repository of formal mathematics.

INRIA-Sophia homepage