Interactive proving and programming in Coq Seminars/Workshops

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.