We have been collecting papers on proof assistant checkers and kernels (and their certification as in MetaCoq) as part of our proof engineering bibliography. 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. A recent take on the classic relative consistency proof of Coq’s foundations is that by Carneiro. See also a relevant Coq wiki page and a bibliography hosted on the wiki.
@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",
}