Up: Cooperating sites
Previous: Novi Sad - Belgrade
Université Paris-Sud
The team at Université Paris Sud in Orsay, France has recognised skills in the development of interactive proof assistants (Coq) but also automatic proof tools based on rewriting (Cime). It has developed specialised tools (Why, Krakatoa) on top of Coq for verification of programs written in C or Java. It is also recognised for its contribution to dependent type theory, in particular modules, combination with rewriting, inductive types and program extraction.
The team will mainly contribute to the objectives of Correctness of Computer Systems and Proof Technology.
- We shall continue our development of environments based on Type Theory dedicated to a specific verification area (mathematics, Java or C programs, automata). It involves to design in type theory good models for the representation of the domain of study, to specialize proof strategies and provides appropriate interface. (Collaboration with Nijmegen, INRIA Sophia-Antipolis, France Telecom, Grenoble).
- We are contributing to the effort to design a usable programming language based on Dependent Type Theory (Collaboration with Chalmers, Durham, Edinburgh and Nottingham).
- We are contributing to the development of the Coq system (Collaboration with INRIA Futurs and the Coq-user sites).
- We are studying the interaction between interactive and automatic proofs in the domain of rewriting and proof of termination (Collaboration with INRIA Futurs, France Telecom).
The senior members are
- Christine Paulin-Mohring, contact person
- Sylvain Conchon
- Evelyne Contejean
- Judicaël Courant
- Jean Duprat (ENS Lyon)
- Jean-Christophe Filliâtre
- Claude Marché
Our research on development of certified Java programs is funded by the IST VERIFICARD project and the national ACI Geccoo. The national project RNTL AVERROES (analysis and verification for the reliability of embedded systems) uses the Coq system for the modelling and verification of systems described by a general class of timed-automata.
Paris Sud homepageBengt Nordström 2005-09-22