| Speaker: | Hugo Herbelin , INRIA |
|---|
| Period: | 2009-06-19 11:00 ~ 2009-06-19 12:00 |
|---|
| Place: | Room 309, Bldg 302, SNU |
|---|
Abstract
Coq is an environment for the semi-interactive development of proofs
with applications to the formalization of mathematical theories and to
the certification of programs. Top applications in Coq are for
instance the full formalization of the 4-color theorem and the full
certification of a realistic C compiler.
Coq is built on a formalism called the Calculus of Inductive
Constructions which is both a logical system of the strength of set
theory and a strongly-typed functional programming languages. We will
show on examples some striking features of Coq.
Short bio
Education:
Dec 2005 Habilitation Diploma, University Paris 11, France
Jan 1995 Ph.D. Theoretical Computer Science, University Paris 7, France
Aug 1989 Agregation in Mathematics (high-school teaching diploma)
Aug 1988 M.S. Computer Science, University Paris 11, France
Research and Work Experience:
Sep 2008 - Present Research Director at INRIA (Coq development and PiR2), France
Sep 2001 - Present Experienced Researcher at INRIA (Coq development), France
Sep 1999 - Aug 2001 On secondment at INRIA, France
Sep 1996 - Aug 1999 Associate Professor, University Paris 10, France
Sep 1993 - Aug 1996 Teaching Assistant, University Paris 7, France
Sep 1990 - Aug 1993 Teaching Assistant, Ecole Normale Supérieure de Lyon, France
Sep 1986 - Aug 1990 Ecole Normale Supérieure de Fontenay-Saint-Cloud, France
Resources
|
