The Coq Proof Assistant A Tutorial Version 1 Gérard Huet, Gilles Kahn and Christine Paulin-Mohring LogiCal Project 1This research was partly supported by IST working group “Types” Getting started Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs