TheoryBehindCoq

Pierre Letouzey edited this page Oct 23, 2017 · 62 revisions
Clone this wiki locally

Introduction

Metatheory of the Calculus of Constructions

Metatheory of Inductive Types

Model Construction

(In)dependence of Axioms

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.