# Interactive proving and programming in Coq Seminars/Workshops

Speaker: | Hugo Herbelin |
---|---|

Time: | 2009-06-19 ~ 19 |

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.

### Resources

[ List ]