ROSAEC center Seoul National University

Seminars & Workshops

Speaker:Hugo Herbelin , INRIA
Period:2009-06-19 11:00 ~ 2009-06-19 12:00
Place:Room 309, Bldg 302, SNU


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

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


© Copyright 2008-2010 ROSAEC Center, Seoul National University