@misc{hales,
  title = {A formal proof of the Kepler conjecture},
  author = {Thomas Hales and Mark Adams and Gertrud Bauer and Dat Tat Dang and John Harrison and Truong Le Hoang and Cezary Kaliszyk and Victor Magron and Sean McLaughlin and Thang Tat Nguyen and Truong Quang Nguyen and Tobias Nipkow and Steven Obua and Joseph Pleso and Jason Rute and Alexey Solovyev and An Hoai Thi Ta and Trung Nam Tran and Diep Thi Trieu and Josef Urban and Ky Khac Vu and Roland Zumkeller},
  year = {2015},
  eprint = {1501.02155},
  archivePrefix = {arXiv},
  primaryClass = {math.MG}
}

@misc{hurry,
  title = {Coq in a Hurry},
  author = {Yves Bertot},
  year = {2008},
  eprint = {cs/0603118},
  archivePrefix = {arXiv},
  primaryClass = {cs.LO}
}

@inproceedings{tactic,
  author = {Delahaye, David},
  editor = {Parigot, Michel and Voronkov, Andrei},
  title = {A Tactic Language for the System Coq},
  booktitle = {Logic for Programming and Automated Reasoning},
  year = {2000},
  publisher = {Springer Berlin Heidelberg},
  address = {Berlin, Heidelberg},
  pages = {85--95},
  abstract = {We propose a new tactic language for the system Coq, which is intended to enrich the current tactic combinators (tacticals). This language is based on a functional core with recursors and matching operators for Coq terms but also for proof contexts. It can be used directly in proof scripts or in toplevel definitions (tactic definitions). We show that the implementation of this language involves considerable changes in the interpretation of proof scripts, essentially due to the matching operators. We give some examples which solve small proof parts locally and some others which deal with non-trivial problems. Finally, we discuss the status of this meta-language with respect to the Coq language and the implementation language of Coq.},
  isbn = {978-3-540-44404-6}
}

@inproceedings{forster,
  author = {Forster, Yannick and Kunze, Fabian and Smolka, Gert and Wuttke, Maximilian},
  title = {A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value $\lambda$-Calculus},
  booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
  year = {2021},
  pages = {19:1--19:20},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-188-7},
  issn = {1868-8969},
  volume = {193},
  editor = {Cohen, Liron and Kaliszyk, Cezary},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/13914},
  urn = {urn:nbn:de:0030-drops-139142},
  doi = {10.4230/LIPIcs.ITP.2021.19},
  annote = {Keywords: formalizations of computational models, computability theory, Coq, time complexity, Turing machines, lambda calculus, Hoare logic}
}

@article{gonthier,
  title = {Formal Proof---The Four-Color Theorem},
  author = {Gonthier, Georges and others},
  journal = {Notices of the AMS},
  volume = {55},
  number = {11},
  pages = {1382--1393},
  year = {2008}
}

@book{whitehead,
  title = {Principia Mathematica to* 56},
  author = {Whitehead, Alfred North and Russell, Bertrand},
  volume = {2},
  year = {1997},
  publisher = {Cambridge University Press}
}

@article{doczkal,
  title = {Graph theory in Coq: Minors, treewidth, and isomorphisms},
  author = {Doczkal, Christian and Pous, Damien},
  journal = {Journal of Automated Reasoning},
  volume = {64},
  pages = {795--825},
  year = {2020},
  publisher = {Springer}
}

@phdthesis{wang,
  title = {Mechanized Verification of Graph-Manipulating Programs},
  author = {Shengyi, Wang},
  year = {2020},
  school = {National University of Singapore (Singapore)}
}

@article{bauer,
  title = {Five stages of accepting constructive mathematics},
  author = {Bauer, Andrej},
  journal = {Bulletin of the American Mathematical Society},
  volume = {54},
  number = {3},
  pages = {481--498},
  year = {2017}
}

@book{ttfp,
  title = {Type Theory and Functional Programming},
  author = {Thompson, Simon},
  year = {1991},
  publisher = {Addison Wesley}
}

@book{coqart,
  title = {Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions},
  author = {Bertot, Yves and Cast{\'e}ran, Pierre},
  year = {2013},
  publisher = {Springer Science \& Business Media}
}

@book{cpdt,
  title = {Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant},
  author = {Chlipala, Adam},
  year = {2022},
  publisher = {MIT Press}
}

@book{sergey,
  title = {Programs and Proofs: Mechanizing Mathematics with Dependent Types},
  author = {Sergey, Ilya},
  year = {2014}
}

@article{ringer2019qed,
  title = {QED at Large: A Survey of Engineering of Formally Verified Software},
  author = {Ringer, Talia and Palmskog, Karl and Sergey, Ilya and Gligoric, Milos and Tatlock, Zachary and others},
  journal = {Foundations and Trends in Programming Languages},
  volume = {5},
  number = {2-3},
  pages = {102--281},
  year = {2019},
  publisher = {Now Publishers, Inc.}
}

@inproceedings{klein2014proof,
  title = {Proof engineering considered essential},
  author = {Klein, Gerwin},
  booktitle = {FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12-16, 2014. Proceedings 19},
  pages = {16--21},
  year = {2014},
  organization = {Springer}
}

@article{girard_paradox,
  title = {Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur},
  author = {Girard, J-Y},
  journal = {Ph. D. Thesis, L'université Paris VII},
  year = {1972}
}

@article{cumulative,
  title = {Cumulative inductive types in Coq},
  author = {Timany, Amin and Sozeau, Matthieu},
  journal = {LIPIcs: Leibniz International Proceedings in Informatics},
  year = {2018},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}
}

@article{wigderson,
  title = {Improving the performance guarantee for approximate graph coloring},
  author = {Wigderson, Avi},
  journal = {Journal of the ACM (JACM)},
  volume = {30},
  number = {4},
  pages = {729--735},
  year = {1983},
  publisher = {ACM New York, NY, USA}
}

@article{wadler,
  title = {Propositions as Types},
  author = {Wadler, Philip},
  journal = {Communications of the ACM},
  volume = {58},
  number = {12},
  pages = {75--84},
  year = {2015},
  publisher = {ACM New York, NY, USA}
}

@book{hott,
  author = {The {Univalent Foundations Program}},
  title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address = {Institute for Advanced Study},
  year = {2013}
}

@book{sf,
  author = {Benjamin C. Pierce and Arthur Azevedo de Amorim and Chris Casinghino and Marco Gaboardi and Michael Greenberg and Cătălin Hriţcu and Vilhelm Sjöberg and Brent Yorgey},
  editor = {Benjamin C. Pierce},
  title = {Logical Foundations},
  series = {Software Foundations},
  volume = {1},
  year = {2023},
  publisher = {Electronic textbook},
  note = {Version 6.3, \URL{http://softwarefoundations.cis.upenn.edu}}
}

@online{wigderson-siraben,
  author = {Siraphob (Ben) Phipathananunth and Jamison Homatas},
  title = {Formalization of Wigderson's graph coloring algorithm in Coq},
  url = {https://github.com/siraben/coq-wigderson},
  urldate = {2023-04-09}
}

@book{mathcomp,
  author = {Assia Mahboubi and Enrico Tassi},
  title = {Mathematical Components},
  publisher = {Zenodo},
  year = {2022},
  month = {September},
  doi = {10.5281/zenodo.7118596},
  url = {https://doi.org/10.5281/zenodo.7118596}
}

@book{hilbert,
  title={Die grundlagen der mathematik: Vortrag, gehalten auf Einladung des Mathematischen Seminars im Juli 1927 in Hamburg},
  author={Hilbert, David},
  year={1928},
  publisher={Springer}
}

@article{church,
  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{coqhammer,
  author = {Czajka, {\L}ukasz and Kaliszyk, Cezary},
  title = {Hammer for Coq: Automation for Dependent Type Theory},
  journal = {Journal of Automated Reasoning},
  year = {2018},
  volume = {61},
  number = {1},
  pages = {423--453},
  month = {Jun.},
  doi = {10.1007/s10817-018-9458-4},
  url = {https://doi.org/10.1007/s10817-018-9458-4},
  issn = {1573-0670},
  language = {English}
}