
# Introduction¶

This document is the Reference Manual of the Coq proof assistant. To start using Coq, it is advised to first read a tutorial. Links to several tutorials can be found at https://coq.inria.fr/documentation and https://github.com/coq/coq/wiki#coq-tutorials

The Coq system is designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specifications. It provides a specification language named Gallina. Terms of Gallina can represent programs as well as properties of these programs and proofs of these properties. Using the so-called Curry-Howard isomorphism, programs, properties and proofs are formalized in the same language called Calculus of Inductive Constructions, that is a $$\lambda$$-calculus with a rich type system. All logical judgments in Coq are typing judgments. The very heart of the Coq system is the type checking algorithm that checks the correctness of proofs, in other words that checks that a program complies to its specification. Coq also provides an interactive proof assistant to build proofs using specific programs called tactics.

All services of the Coq proof assistant are accessible by interpretation of a command language called the vernacular.

Coq has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where commands are processed from a file.

• In interactive mode, users can develop their theories and proofs step by step, and query the system for available theorems and definitions. The interactive mode is generally run with the help of an IDE, such as CoqIDE, documented in Coq Integrated Development Environment, Emacs with Proof-General [Asp00] [1], or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). The coqtop read-eval-print-loop can also be used directly, for debugging purposes.
• The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, Coq’s compiler provides an output file containing a compact representation of its input. The compiled mode is run with the coqc command.