MR3468261

Paulin-Mohring, Christine

Introduction to the calculus of inductive constructions.

All about proofs, proofs for all, 116--133, Stud. Log. (Lond.), 55, Coll. Publ., London, 2015. 03B35 (03F07 68N15)

The paper is a recent introduction to the features of the calculus of inductive constructions, the formal logic underlying the Coq proof assistant software. Some historical perspective as well as comments on the present and future developments of the formalism and Coq is also given.

For the sake of historical completeness, it would have probably been worthwhile to mention the much earlier work in proof theory of constructive systems, a direct precursor of the theory around Coq, such as summarized for instance in Troelstra's 1973 book "Metamathematical Investigation of Intuitionistic Arithmetic and Analysis".