This tutorial is no longer maintained. See our documentation page for more recent references.

An invitation to Coq. It is a commented interactive session which introduces basics on terms, proofs, and tactics.


Authors : Gérard Huet, Gilles Kahn and Christine Paulin-Mohring
©INRIA 1999-2004 (Coq versions 7.x)
©INRIA 2004-2017 (Coq versions 8.x)
This research was partly supported by IST working group “Types”.