Abstract
The last lecture of the year took the form of an introspection. Throughout the lecture, we used a demonstration assistant (Coq) as a language and verification tool. How can we formalize and mechanize the semantic correction of such a tool ? This immediately raises the question of the consistency of the logic implemented by the tool. A logic is coherent if it cannot derive paradoxes or other absurd statements.
For a logic based on type theory, such as Coq's, coherence corresponds, in the Curry-Howard sense, to the existence of a type that is not inhabited (no closed term belongs to this type). We have outlined a Curry-Howard-style consistency proof, which extends the safety proof seen in the previous lecture with a new imperative : the normalization property, " any well-typed term ends ". Normalization is demonstrated using logical relations. However, impredicative type systems such as F easily lead to ill-defined, circular logical relations. Girard's " reducibility candidates" technique avoids this circularity.
From the F system to Coq and Agda, the path is a long one, involving the addition of dependent types, type operators, inductive or coinductive types, and a hierarchy of universes. Significant fragments of Coq logic have been formalized and verified in Coq, sometimes demonstrating normalization, often admitting it. Similarly, fragments of Agda have been formalized in Agda following an intrinsically typed syntax approach.
Will we ever be able to " verify Coq in Coq ", i.e. to demonstrate the logical consistency of Coq by means of a mechanized demonstration in Coq ? Gödel's second incompleteness theorem tells us that this is strictly speaking impossible. But it seems plausible that a large fragment of Coq or Agda could be verified using a barely larger fragment, which would constitute a magnificent " self-priming " of these demonstration assistants.
