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

• talk slide