# Understanding the Coq kernel

**URL:** <https://discourse.rocq-prover.org/t/understanding-the-coq-kernel/293>\
**Category:** Using Rocq\
**Created:** [May 19, 2019, 2:25pm UTC](https://discourse.rocq-prover.org/t/understanding-the-coq-kernel/293 "2019-05-19T14:25:27Z")\
**Posts on this page:** 1\
**Showing post:** 4

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [May 23, 2019, 11:44pm UTC](https://discourse.rocq-prover.org/t/understanding-the-coq-kernel/293/4 "2019-05-23T23:44:06Z")

</div>

We have been collecting papers on proof assistant checkers and kernels (and their certification as in MetaCoq) as part of our [proof engineering bibliography](https://github.com/proofengineering/proofengineering-bib). Below are some highlights not mentioned in preceding replies.

The best source for the general history of Coq and its kernel (up to 2004) is the foreword by Huet and Paulin-Mohring to the [Coq’Art book](https://link.springer.com/book/10.1007/978-3-662-07964-5). A recent take on the classic relative consistency proof of Coq’s foundations is that by [Carneiro](https://github.com/digama0/lean-type-theory). See also a relevant [Coq wiki page](https://github.com/coq/coq/wiki/TheoryBehindCoq) and a [bibliography](https://raw.githubusercontent.com/wiki/coq/coq/files/biblio.bib) hosted on the wiki.

```auto
@techreport{Filliatre2000,
  author = "Jean-Christophe Filli\^atre",
  title = "Design of a proof assistant: {Coq} version 7",
  institution = "LRI, Universit\'e Paris Sud",
  type = "Research Report",
  number = 1369,
  month = oct,
  year = 2000,
  url = "http://www.lri.fr/~filliatr/ftp/publis/coqv7.ps.gz",
}

@InProceedings{Asperti2007,
author="Asperti, Andrea
and Coen, Claudio Sacerdoti
and Tassi, Enrico
and Zacchiroli, Stefano",
title="Crafting a Proof Assistant",
booktitle="Types for Proofs and Programs",
year="2007",
publisher="Springer",
pages="18--32",
isbn="978-3-540-74464-1",
doi="10.1007/978-3-540-74464-1_2",
}

@InProceedings{Harrison2006,
author="Harrison, John",
title="Towards Self-verification of {HOL Light}",
booktitle="Automated Reasoning",
year="2006",
publisher="Springer",
pages="177--191",
isbn="978-3-540-37188-5",
doi="10.1007/11814771_17",
}

@Article{Kumar2016,
author="Kumar, Ramana
and Arthan, Rob
and Myreen, Magnus O.
and Owens, Scott",
title="Self-Formalisation of Higher-Order Logic",
journal="Journal of Automated Reasoning",
year="2016",
month="Mar",
day="01",
volume="56",
number="3",
pages="221--259",
issn="1573-0670",
doi="10.1007/s10817-015-9357-x",
}

@phdthesis{Kumar2015,
  author = "Ramana Kumar",
  title = "Self-compilation and self-verification",
  year = "2015",
  school = "University of Cambridge",
  url = "https://www.cl.cam.ac.uk/~rk436/thesis.pdf",
}

@Article{Davis2015,
author="Davis, Jared
and Myreen, Magnus O.",
title="The Reflective {Milawa} Theorem Prover is Sound (Down to the Machine Code that Runs it)",
journal="Journal of Automated Reasoning",
year="2015",
volume="55",
number="2",
pages="117--183",
issn="1573-0670",
doi="10.1007/s10817-015-9324-6",
}

@techreport{Pollack1997,
  title = "How to Believe a Machine-Checked Proof",
  author = "Robert Pollack",
  year = "1997",
  month = "July",
  number = "BRICS RS-97-18",
  institution = "Department of Computer Science, University of Aarhus",
  address = "Aarhus, Denmark",
  url = "http://www.brics.dk/RS/97/18/BRICS-RS-97-18.pdf",
}

@article{Adams2016b,
  author = "Mark Adams",
  title = "Proof Auditing Formalised Mathematics",
  journal = "Journal of Formalized Reasoning",
  volume = "9",
  number = "1",
  year = "2016",
  issn = "1972-5787",
  pages = "3--32",
  doi = "10.6092/issn.1972-5787/4576",
  url = "https://jfr.unibo.it/article/view/4576"
}

@InProceedings{Adams2016,
author="Adams, Mark",
editor="Blanchette, Jasmin Christian
and Merz, Stephan",
title="{HOL Zero's} Solutions for {Pollack-Inconsistency}",
booktitle="Interactive Theorem Proving",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="20--35",
isbn="978-3-319-43144-4",
doi="10.1007/978-3-319-43144-4_2",
}

@article{Wiedijk2012,
title = "Pollack-inconsistency",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "285",
pages = "85--100",
year = "2012",
note = "",
issn = "1571-0661",
doi = "10.1016/j.entcs.2012.06.008",
url = "http://www.sciencedirect.com/science/article/pii/S157106611200028X",
author = "Freek Wiedijk",
}

@InProceedings{Werner1997,
author="Werner, Benjamin",
title="Sets in types, types in sets",
booktitle="Theoretical Aspects of Computer Software",
year="1997",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="530--546",
isbn="978-3-540-69530-1",
doi="10.1007/BFb0014566",
}

@article{Barras2010,
  author = "Bruno Barras",
  title = "Sets in {Coq}, {Coq} in Sets",
  journal = "Journal of Formalized Reasoning",
  volume = "3",
  number = "1",
  year = "2010",
  issn = "1972-5787",
  pages = "29--48",
  doi = "10.6092/issn.1972-5787/1695",
  url = "https://jfr.unibo.it/article/view/1695",
}

@InProceedings{Anand2014,
author="Anand, Abhishek and Rahli, Vincent",
title="Towards a Formally Verified Proof Assistant",
booktitle="Interactive Theorem Proving",
year="2014",
publisher="Springer International Publishing",
address="Cham",
pages="27--44",
isbn="978-3-319-08970-6",
doi="10.1007/978-3-319-08970-6_3",
}

@article{Coquand1988,
title = "The calculus of constructions",
journal = "Information and Computation",
volume = "76",
number = "2",
pages = "95--120",
year = "1988",
issn = "0890-5401",
doi = "10.1016/0890-5401(88)90005-3",
url = "http://www.sciencedirect.com/science/article/pii/0890540188900053",
author = "Thierry Coquand and G{\'e}rard Huet"
}

@InProceedings{Coquand1990,
author="Coquand, Thierry
and Paulin-Mohring, Christine",
editor="Martin-L{\"o}f, Per
and Mints, Grigori",
title="Inductively defined types",
booktitle="COLOG-88",
year="1990",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="50--66",
isbn="978-3-540-46963-6",
doi="10.1007/3-540-52335-9_47",
}

@InProceedings{PaulinMohring1993,
author="Paulin-Mohring, Christine",
editor="Bezem, Marc
and Groote, Jan Friso",
title="Inductive definitions in the system {Coq} rules and properties",
booktitle="Typed Lambda Calculi and Applications",
year="1993",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="328--345",
isbn="978-3-540-47586-6",
doi="10.1007/BFb0037116"
}

@inbook{Coquand1990b,
  author = "Thierry Coquand",
  title = "Metamathematical investigations of a calculus of constructions",
  booktitle = "Logic and Computer Science",
  publisher = "Academic Press",
  year = "1990",
  pages = "91-122",
  editor = "P. Odifreddi",
  url = "http://www.cse.chalmers.se/~coquand/meta.pdf",
}

```

---

_[View the full topic](https://discourse.rocq-prover.org/t/understanding-the-coq-kernel/293)._