TheoryBehindCoq

Introduction

• Introductions to the type theory

  Type Theory and Functional Programming, by Simon Thompson

  Type Theory and Formal Proof, by Herman Geuvers and Rob Nederpelt - primarily focuses on the Calculus of Constructions

  Introduction to the Calculus of Inductive Constructions, by Christin Paulin-Mohring

• Lectures about Coq

  http://www.europeindia.org/cd09/lectures/lect04/index.htm

  Lecture notes by Femke van Raamsdonk

  Lecture notes on Lambda calculus, types and their use in proofs, by Yves Bertot (in French)

Metatheory of the Calculus of Constructions

• Metamathematical Investigations of a Calculus of Construction, Thierry Coquand

Metatheory of Inductive Types

• Definitions and further issues regarding inductive types in Coq, Christine Paulin (in French)

  In this work the definitions based on case (case analysis, now called match) and Fixpoint are described. Several issues eg. mutual inductive types, restrictions on elimination sort and positivity condition are studied.

• Guardedness condition for fixed points and cofixed points, Eduardo Giménez

Model Construction

• Realizability model for the calculus of construction with universes (CC_{omega}) with subtyping, Alexandre Miquel

  This paper contains realizability model for a system stronger than Coq but without inductive types.

• Set-theoretical model of the calculus of construction (CC) and discussion about the extension to CC_{omega}, Alexandre Miquel and Benjamin Werner

• Realizability model for the calculus of construction (CC) extended with the type of natural numbers and only one universe, Benjamin Werner (in French)

• Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC), Sozeau and Timany Set theoretical model for pCIC with universe polymorphic inductive types. also conjectures SN.

(In)dependence of Axioms

• Groupoid model of intensional Martin-Lof type theory, Martin Hofmann and Thomas Streicher: This shows the independence of Axiom K, which states that there is only one proof of reflexivity statement.
• Excluded Middle in impredicative Set and extensionality of functions are refuted by Miquel's realizability model of CC_{omega}, Alexandre Miquel
• Excluded Middle in Prop and Axiom of Choice in Type are inconsistent with impredicative Set, Laurent Chicli and Loïc Pottier and Carlos Simpson
• Unprovability of many extensionality principles
• Unprovability of Markov's principle and negation of function extensionality

Others

• Why does Coq use inductive types and not W-Types?
• A summary of the long and informative discussion that took place on the coq-club mailing list when similar bugs were discovered in the termination checkers of both Coq and Agda.
• Some proof theoretic consequences of impredicative Prop.
• Definitional Proof-Irrelevance Without K - theoretical justification for SProp, the sort of strict propositions