The Certilab team
Formal Specification, Certified Software
Our group is interested in formal specification, certified software
and program validation.
For a detailed presentation of our objectives, see
here
(in french).
Team's members:
- Researchers:
- PhD students:
- Secretary:
- Former PhD students:
Members of the TYPES
site at INRIA Sophia Antipolis:
- INRIA Sophia Antipolis:
Gilles Barthe, Yves Bertot, Joëlle Despeyroux, André Hirschowitz,
Loïc Pottier, Laurent Thery,
Laurent Chicli, Guillaume Gillard, Hanane Naciri, Simão de Sousa,
- Associated site:
Minho, Portugal:
Luis Pinto, Maria Joao Frade, Jose Bacelar Almeida,
Jose Espirito Santo, Tarmo Uustalu, Olivier Pons and Jorge Sousa Pinto,
- Industrial site:
Dassault-Aviation:
Emmanuel Ledinot.
Selected events:
-
Journal of Functional Programming
special issue
on Logical Frameworks and Meta-languages.
The submission deadline was October 23, 2000.
-
Past events:
- LFM'00. The
workshop on Logical Frameworks and Meta-languages was held on Sunday,
June 25, 2000, at Santa Barbara, California.
- Types'99.
The "Types" summer school has been held on French Riviera, France,
from August 30 to September 10, 1999.
Teaching:
-
We are giving a graduate course
on secure software
at the
Dea in CS, University of Nice Sophia-Antipolis (UNSA).
Starting Fall 2000.
This course is a subpart of the course that has been proposed for a master
on "formal methods and certified software"
at the same university.
-
We are giving a graduate course
on mechanization of proofs
at the
Dea in CS, University of Nice Sophia-Antipolis (UNSA).
-
We are also giving a graduate course on
"Natural Semantics: Specifications and Proofs",
at the Dea MDFI
("Mathématiques Discrètes et Fondements de l'Informatique") at Marseille,
since Dec. 1995;
lecture notes in french, 80 pages.
New course started in 99-00: Mechanization of proofs
(résumé).
Some
pictures from conferences or summer schools.
Inria web page for
Certilab.
Joelle Despeyroux
Last modified: Tue Jun 5 16:07:22 MEST 2001