@book{andrews2013introduction,
  title={An introduction to mathematical logic and type theory: to truth through proof},
  author={Andrews, Peter B.},
  volume={27},
  year={2013},
  edition = {2nd},
  series={Applied Logic Series},
  publisher={Springer Science \& Business Media}
}

@inproceedings{DBLP:conf/itp/AbrahamssonMKS22,
  author       = {Oskar Abrahamsson and
                  Magnus O. Myreen and
                  Ramana Kumar and
                  Thomas Sewell},
  editor       = {June Andronick and
                  Leonardo de Moura},
  title        = {Candle: {A} Verified Implementation of {HOL Light}},
  booktitle    = {13th International Conference on Interactive Theorem Proving, {ITP}
                  2022, August 7-10, 2022, Haifa, Israel},
  series       = {LIPIcs},
  volume       = {237},
  pages        = {3:1--3:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2022},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2022.3},
  doi          = {10.4230/LIPIcs.ITP.2022.3},
  timestamp    = {Mon, 26 Jun 2023 20:47:39 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AbrahamssonMKS22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jar/KumarAMO16,
  author       = {Ramana Kumar and
                  Rob Arthan and
                  Magnus O. Myreen and
                  Scott Owens},
  title        = {Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and
                  a Verified Implementation},
  journal      = {J. Autom. Reason.},
  volume       = {56},
  number       = {3},
  pages        = {221--259},
  year         = {2016},
  url          = {https://doi.org/10.1007/s10817-015-9357-x},
  doi          = {10.1007/s10817-015-9357-x},
  timestamp    = {Wed, 02 Sep 2020 13:29:45 +0200},
  biburl       = {https://dblp.org/rec/journals/jar/KumarAMO16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/KumarAMO14,
  author       = {Ramana Kumar and
                  Rob Arthan and
                  Magnus O. Myreen and
                  Scott Owens},
  editor       = {Gerwin Klein and
                  Ruben Gamboa},
  title        = {{HOL} with Definitions: Semantics, Soundness, and a Verified Implementation},
  booktitle    = {Interactive Theorem Proving - 5th International Conference, {ITP}
                  2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
                  Austria, July 14-17, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8558},
  pages        = {308--324},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-319-08970-6\_20},
  doi          = {10.1007/978-3-319-08970-6\_20},
  timestamp    = {Tue, 14 May 2019 10:00:37 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/KumarAMO14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AbrahamssonM23,
  author       = {Oskar Abrahamsson and
                  Magnus O. Myreen},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Fast, Verified Computation for {Candle}},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {4:1--4:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.4},
  doi          = {10.4230/LIPICS.ITP.2023.4},
  timestamp    = {Wed, 26 Jul 2023 17:17:16 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AbrahamssonM23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Harrison06,
  author       = {John Harrison},
  editor       = {Ulrich Furbach and
                  Natarajan Shankar},
  title        = {Towards Self-verification of {HOL Light}},
  booktitle    = {Automated Reasoning, Third International Joint Conference, {IJCAR}
                  2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {4130},
  pages        = {177--191},
  publisher    = {Springer},
  year         = {2006},
  url          = {https://doi.org/10.1007/11814771\_17},
  doi          = {10.1007/11814771\_17},
  timestamp    = {Thu, 05 Sep 2019 14:51:32 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Harrison06.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{Metalogic_ProofChecker-AFP,
  author  = {Tobias Nipkow and Simon Ro{\ss}kopf},
  title   = {Isabelle's Metalogic: Formalization and Proof Checker},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/Metalogic_ProofChecker.html},
             Formal proof development},
  ISSN    = {2150-914x},
}

@article{DBLP:journals/jar/RosskopfN23,
  author       = {Simon Ro{\ss}kopf and
                  Tobias Nipkow},
  title        = {A Formalization and Proof Checker for {Isabelle's} Metalogic},
  journal      = {J. Autom. Reason.},
  volume       = {67},
  number       = {1},
  pages        = {1},
  year         = {2023},
  url          = {https://doi.org/10.1007/s10817-022-09648-w},
  doi          = {10.1007/s10817-022-09648-w},
  timestamp    = {Tue, 28 Feb 2023 10:48:15 +0100},
  biburl       = {https://dblp.org/rec/journals/jar/RosskopfN23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/NipkowR21,
  author       = {Tobias Nipkow and
                  Simon Ro{\ss}kopf},
  editor       = {Andr{\'{e}} Platzer and
                  Geoff Sutcliffe},
  title        = {Isabelle's Metalogic: Formalization and Proof Checker},
  booktitle    = {Automated Deduction - {CADE} 28 - 28th International Conference on
                  Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12699},
  pages        = {93--110},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-79876-5\_6},
  doi          = {10.1007/978-3-030-79876-5\_6},
  timestamp    = {Thu, 29 Jul 2021 13:42:16 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/NipkowR21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cpp/KochK22,
  author       = {Mark Koch and
                  Dominik Kirst},
  editor       = {Andrei Popescu and
                  Steve Zdancewic},
  title        = {Undecidability, incompleteness, and completeness of second-order logic
                  in Coq},
  booktitle    = {{CPP} '22: 11th {ACM} {SIGPLAN} International Conference on Certified
                  Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022},
  pages        = {274--290},
  publisher    = {{ACM}},
  year         = {2022},
  url          = {https://doi.org/10.1145/3497775.3503684},
  doi          = {10.1145/3497775.3503684},
  timestamp    = {Sat, 30 Sep 2023 09:37:48 +0200},
  biburl       = {https://dblp.org/rec/conf/cpp/KochK22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ictac/Obua06,
  author       = {Steven Obua},
  editor       = {Kamel Barkaoui and
                  Ana Cavalcanti and
                  Antonio Cerone},
  title        = {Partizan Games in {Isabelle/HOLZF}},
  booktitle    = {Theoretical Aspects of Computing - {ICTAC} 2006, Third International
                  Colloquium, Tunis, Tunisia, November 20-24, 2006, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {4281},
  pages        = {272--286},
  publisher    = {Springer},
  year         = {2006},
  url          = {https://doi.org/10.1007/11921240\_19},
  doi          = {10.1007/11921240\_19},
  timestamp    = {Mon, 21 Feb 2022 14:40:49 +0100},
  biburl       = {https://dblp.org/rec/conf/ictac/Obua06.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{ZFC_in_HOL-AFP,
  author  = {Lawrence C. Paulson},
  title   = {Zermelo {Fraenkel} Set Theory in Higher-Order Logic},
  journal = {Archive of Formal Proofs},
  month   = {October},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/ZFC_in_HOL.html},
             Formal proof development},
  ISSN    = {2150-914x},
}

@article{DBLP:journals/pacmpl/SozeauBFTW20,
  author       = {Matthieu Sozeau and
                  Simon Boulier and
                  Yannick Forster and
                  Nicolas Tabareau and
                  Th{\'{e}}o Winterhalter},
  title        = {{Coq} {Coq} correct! verification of type checking and erasure for {Coq},
                  in {Coq}},
  journal      = {Proc. {ACM} Program. Lang.},
  volume       = {4},
  number       = {{POPL}},
  pages        = {8:1--8:28},
  year         = {2020},
  url          = {https://doi.org/10.1145/3371076},
  doi          = {10.1145/3371076},
  timestamp    = {Sat, 30 Sep 2023 10:23:24 +0200},
  biburl       = {https://dblp.org/rec/journals/pacmpl/SozeauBFTW20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Barras96,
  author       = {Bruno Barras},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Verification of the Interface of a Small Proof System in {Coq}},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {28--45},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097785},
  doi          = {10.1007/BFB0097785},
  timestamp    = {Tue, 14 May 2019 10:00:42 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Barras96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@techreport{barras:inria-00073667,
  TITLE = {{Coq en Coq}},
  AUTHOR = {Barras, Bruno},
  URL = {https://inria.hal.science/inria-00073667},
  NOTE = {Projet COQ, \url{https://inria.hal.science/inria-00073667}},
  TYPE = {Research Report},
  NUMBER = {RR-3026},
  INSTITUTION = {{INRIA}},
  YEAR = {1996},
  KEYWORDS = {TYPE THEORY ; METATHEORY ; CALCULUS OF CONSTRUCTIONS ; PROGRAM EXTRACTION},
  PDF = {https://inria.hal.science/inria-00073667/file/RR-3026.pdf},
  HAL_ID = {inria-00073667},
  HAL_VERSION = {v1},
}

@techreport{coqincoqmanuscript,
  title = {{Coq} in {Coq} (manuscript)},
  author = {Bruno Barras and Benjamin Werner},
  year = {1996},
  note = {\url{http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf}}
}

@inproceedings{coqincoqcontribs,
  title={coq-in-coq},
  author={Bruno Barras},
  booktitle={coq-contribs},
  note={\url{https://github.com/coq-contribs/coq-in-coq}},
  year={1997}
}

@misc{arthan1993,
  title={{HOL} Formalised: Language and Overview},
  author={Arthan, Rob},
  year={1993, revised 2014},
  note={\url{http://www.lemma-one.com/ProofPower/specs/specs.html}}
}

@misc{arthan1991sem,
  title={{HOL} Formalised: Semantics},
  author={Arthan, Rob},
  year={1993, revised 2014},
  note={\url{http://www.lemma-one.com/ProofPower/specs/specs.html}}
}

@misc{arthan1991ded,
  title={{HOL} Formalised: Deductive System},
  author={Arthan, Rob},
  year={1993, revised 2002},
  note={\url{http://www.lemma-one.com/ProofPower/specs/specs.html}}
}

@article{russell1908mathematical,
  title={Mathematical logic as based on the theory of types},
  author={Russell, Bertrand},
  journal={American journal of mathematics},
  volume={30},
  number={3},
  pages={222--262},
  year={1908}
}

@book{whiteheadrussel,
  title={Principia Mathematica},
  author={Alfred North Whitehead and Bertrand Russell},
  publisher={Cambridge University Press, Cambridge England},
  year={1913},
  note={3 volumes; first edition 1913, second edition 1927}
}

@article{church1940formulation,
  title={A formulation of the simple theory of types},
  author={Church, Alonzo},
  journal={The journal of symbolic logic},
  volume={5},
  number={2},
  pages={56--68},
  year={1940},
  publisher={Cambridge University Press}
}
  
@article{henkin1950completeness,
  title={Completeness in the theory of types},
  author={Henkin, Leon},
  journal={The Journal of Symbolic Logic},
  volume={15},
  number={2},
  pages={81--91},
  year={1950},
  publisher={Cambridge University Press}
}

@article{henkin1963b,
  title={A Theory of Propositional Types},
  author={Henkin, Leon},
  journal={Fundamenta Mathematicae},
  volume={52},
  pages={323--344},
  year={1963}
}

@article{andrews1963reduction,
  title={A reduction of the axioms for the theory of propositional types},
  author={Andrews, Peter},
  journal={Fundamenta Mathematicae},
  volume={52},
  pages={345--350},
  year={1963}
}

@article{andrews1972general,
  title={General models and extensionality},
  author={Andrews, Peter B},
  journal={The Journal of Symbolic Logic},
  volume={37},
  number={2},
  pages={395--397},
  year={1972},
  publisher={Cambridge University Press}
}

@article{Q0_Metatheory-AFP,
  author  = {Javier D{\'i}az},
  title   = {Metatheory of {Q0}},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/Q0_Metatheory.html},
             Formal proof development},
  ISSN    = {2150-914x},
}

@article{Q0IsaFoL,
  author  = {Anders Schlichtkrull},
  title   = {Q0},
  journal = {IsaFoL},
  year    = {Jan 4th 2022 - Nov 2023},
  note    = {Now at GitHub \url{https://github.com/IsaFoL/IsaFoL/tree/master/Q0} but formerly at BitBucket \url{https://bitbucket.org/isafol/isafol/src/master/Q0/}.
             Formal proof development}
}


