Interactive proving and programming in Coq Seminars/Workshops
|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 ]