What is Coq?

Coq is a proof assistant, i.e., a program used by mathematicians/computer scientists to formalize mathematical theories and proofs. Coq checks proofs and only accepts correct ones. Using Coq provides the highest level of assurance in correctness of proofs.

Why Coq?

In the LogSem research group we study programs, programming languages and compilers. We use very detailed mathematical models for studying these systems. This makes proofs complicated and error-prone. Using a proof assistant like Coq helps ensure that proofs are correct, e.g., no corner case is forgotten.

Curry-Howard correspondence

The Curry-Howard correspondence, discovered by Haskell B. Curry and William A. Howard, is a relationship between programming languages and logics. This correspondence states that mathematical theorems can be expressed as types of a sufficiently expressive programming language. Moreover, programs whose type correspond to a theorem T correspond to proofs of T. Hence, the compiler which checks well-typedness of programs can be used to check correctness of proofs.

The following table shows the correspondence for some logical connectives:

In Logic	In Types	Intuition
True: ⊤	the unit type: ()	There is only one proof of ⊤.
False: ⊥	the empty type	There is no proof of ⊥.
implication: P → Q	function types: P → Q	A proof of P → Q is a function that takes a proof of P and returns a proof of Q.
conjunction: P ∧ Q	product types (pairs): P * Q	A proof of P ∧ Q is a pair of proofs, one of P and the other of Q.
disjunction: P ∨ Q	sum types (tagged unions): P + Q	A proof of P ∨ Q consists of a label (left or right disjunct) together with a proof of P (in the left case), or a proof of Q (in the right case).
universal quantification: ∀ x, P(x)	dependent function types (see below)*: Π x : T, P(x)	A proof of ∀ x, P(x) is a dependent function that given an a returns z proof of P(z).
universal quantification: ∃ x, P(x)	dependent record types: {x : T; p : P(x)}	A proof of ∃ x, P(x) is a dependent record where the first field is a witness z and the second field is a proof of P(z).

^* Note how in a depdendent function type the argument x whose type is T can appear in the type of codomain, P.

Coq as a programming language and a logic

At its core, Coq is based on the predicative calculus of cumulative inductive constructions (pCuIC). The system pCuIC is a lambda coalculus with a very expressive type system. Coq allows programmers/mathematicians to write programs in Gallina (this is essentially a programming langae corresponding to the system pCuIC). In Gallina, the user can define constructions, i.e., types and programs. The type system of Coq (and pCuIC) is a so-called dependent type theory where one can write so-called dependent function whose output type depends on the input, e.g., a program that takes a list l and returns a list that is the sorted version of that list (a program whose type essentially establishes its correctness!), or a function that given a number n returns a proof (recall that a proof is just a program) that 2 * (1 + 2 + ... + n) = n * (n + 1). In particular, in a dependent type theory one can write a program that computes the type and then write a program of that type.

All these features will be made clear once we take a closer look at Coq and see a few examples.

Expressivity of Coq and pCuIC

The expressivity of pCuIC's type system enables formalization of serious mathematical theories. Very impressive mathematical theorems have been formalized and machine-checked in Coq, e.g., the famous four-color theorem, The verified C compiler CompCert, etc.