Speaker: Hugo Herbelin
Time:2009-06-19 ~ 19
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.


[ List ]