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-2006 (Coq versions 8.x)
This research was partly supported by IST working group “Types”.