The Coq Proof Assistant

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

Index

• Getting started
• Chapter 1 Basic Predicate Calculus
• Chapter 2 Induction
• Chapter 3 Modules

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”.