@article(DBLP-journals/pacmpl/0001OV18,
 author       = {Andreas Abel and Joakim {\"{O}}hman and Andrea Vezzosi},
 year         = {2018},
 title        = {Decidability of conversion for type theory in type theory},
 journal      = {{PACMPL}},
 volume       = {2},
 number       = {{POPL}},
 pages        = {23:1--23:29},
 doi          = {10.1145/3158111},
)
@article(DBLP:journals/cj/AkbarpourATH10,
 author       = {Behzad Akbarpour and Abdel{-}Hamid, Amr T. and Sofi{\`{e}}ne Tahar and John Harrison},
 year         = {2010},
 title        = {Verifying a Synthesized Implementation of {IEEE-754} Floating-Point Exponential Function using {HOL}},
 journal      = {Comput. J.},
 volume       = {53},
 number       = {4},
 pages        = {465--488},
 doi          = {10.1093/comjnl/bxp023},
)
@phdthesis(alti:phd93,
 author       = {Thorsten Altenkirch},
 year         = {1993},
 title        = {Constructions, Inductive Types and Strong Normalization},
 school       = {University of Edinburgh},
)
@inproceedings(certicoq.CoqPL,
 author       = {Abhishek Anand and Andrew Appel and Greg Morrisett and Zoe Paraskevopoulou and Randy Pollack and Olivier Savary Belanger and Matthieu Sozeau and Matthew Weaver},
 year         = {2017},
 title        = {{CertiCoq: A verified compiler for Coq}},
 booktitle    = {CoqPL},
 address      = {Paris, France},
)
@book(DBLP:books/daglib/0034962,
 author       = {Andrew W. Appel},
 year         = {2014},
 title        = {Program Logics - for Certified Compilers},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781107256552},
)
@inproceedings(armand2010itp,
 author       = {Micha{\"e}l Armand and Benjamin Gr{\'e}goire and Arnaud Spiwack and Laurent Th{\'e}ry},
 year         = {2010},
 title        = {Extending Coq with Imperative Features and Its Application to SAT Verification},
 editor       = {Matt Kaufmann and Lawrence C. Paulson},
 booktitle    = {Interactive Theorem Proving},
 publisher    = {Springer},
 pages        = {83--98},
 doi          = {10.1016/j.jal.2007.07.003},
)
@phdthesis(Barras99,
 author       = {Bruno Barras},
 year         = {1999},
 title        = {Auto-validation d'un syst{\`e}me de preuves avec familles inductives},
 type         = {Th{\`e}se de doctorat},
 school       = {Universit{\'e} Paris~7},
)
@unpublished(barras-habilitation,
 author       = {Bruno Barras},
 year         = {2012},
 title        = {Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families},
 note         = {Unpublished},
)
@inproceedings(DBLP.conf/cpp/BauerGLSSS17,
 author       = {Andrej Bauer and Jason Gross and Peter LeFanu Lumsdaine and Michael Shulman and Matthieu Sozeau and Bas Spitters},
 year         = {2017},
 title        = {The HoTT library: a formalization of homotopy type theory in Coq},
 editor       = {Yves Bertot and Viktor Vafeiadis},
 booktitle    = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs and Proofs, {CPP} 2017, Paris, France, January 16-17, 2017},
 publisher    = {ACM},
 pages        = {164--172},
 doi          = {10.1145/3018610.3018615},
)
@article(journals/talg/BenderFGT16,
 author       = {Michael A. Bender and Jeremy T. Fineman and Seth Gilbert and Robert E. Tarjan},
 year         = {2016},
 title        = {A New Approach to Incremental Cycle Detection and Related Problems},
 journal      = {{ACM} Trans. Algorithms},
 volume       = {12},
 number       = {2},
 pages        = {14:1--14:22},
 doi          = {10.1145/2756553},
)
@inproceedings(DBLP:conf/itp/BertholonMR19,
 author       = {Guillaume Bertholon and Martin{-}Dorel, {\'{E}}rik and Pierre Roux},
 year         = {2019},
 title        = {Primitive Floats in Coq},
 editor       = {John Harrison and John O'Leary and Andrew Tolmach},
 booktitle    = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}},
 series       = {LIPIcs},
 volume       = {141},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {7:1--7:20},
 doi          = {10.4230/LIPIcs.ITP.2019.7},
)
@article(liesnikov2020,
 author       = {Bohdan Liesnikov, Marcel Ullrich and Yannick Forster},
 year         = {2020},
 title        = {Generating induction principles and subterm relations for inductive types using MetaCoq},
 journal      = {The Coq Workshop 2020},
)
@article(DBLP:journals/entcs/Chapman09,
 author       = {James Chapman},
 year         = {2009},
 title        = {Type Theory Should Eat Itself},
 journal      = {Electron. Notes Theor. Comput. Sci.},
 volume       = {228},
 pages        = {21--36},
 doi          = {10.1016/j.entcs.2008.12.114},
)
@inproceedings(DBLP:conf/cpp/Chlipala20,
 author       = {Adam Chlipala},
 year         = {2020},
 title        = {Proof assistants at the hardware-software interface (invited talk)},
 editor       = {Jasmin Blanchette and Catalin Hritcu},
 booktitle    = {{CPP} 2020},
 publisher    = {{ACM}},
 pages        = {2},
 doi          = {10.1145/3372885.3378575},
)
@article(COQUAND88,
 author       = {Thierry Coquand and G\'{e}rard Huet},
 year         = {1988},
 title        = {The {C}alculus of {C}onstructions},
 journal      = {Information and Computation},
 volume       = {76},
 number       = {2--3},
 pages        = {95--120},
 doi          = {10.1016/0890-5401(88)90005-3},
)
@techreport(filliatre:hal-02890416,
 author       = {Jean-Christophe Filli{\^a}tre},
 year         = {2000},
 title        = {{Design of a proof assistant: Coq version 7}},
 type         = {Research Report},
 institution  = {{Universit{\'e} Paris-Sud}},
)
@misc(filliatr2020coqws,
 author       = {Jean-Christophe Filli{\^a}tre},
 year         = {2020},
 title        = {A Coq retrospective, at the heart of Coq architecture, the genesis of version 7.0},
 howpublished = {Invited talk at the Coq Workshop 2020},
)
@misc(compcert,
 author       = {Gallium and Marelle and CEDRIC and PPS},
 year         = {2008},
 title        = {The {C}omp{C}ert project},
 howpublished = {Compilers You Can \emph{Formally} Trust},
)
@inproceedings(DBLP-conf/icalp/Gimenez98,
 author       = {Eduardo Gim{\'e}nez},
 year         = {1998},
 title        = {Structural Recursive Definitions in Type Theory},
 editor       = {Kim Guldstrand Larsen and Sven Skyum and Glynn Winskel},
 booktitle    = {ICALP},
 series       = {LNCS},
 volume       = {1443},
 publisher    = {Springer},
 pages        = {397--408},
)
@inproceedings(DBLP:conf/itp/GonthierAABCGRMOBPRSTT13,
 author       = {Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and Cyril Cohen and Fran{\c{c}}ois Garillot and St{\'{e}}phane Le Roux and Assia Mahboubi and Russell O'Connor and Sidi Ould Biha and Ioana Pasca and Laurence Rideau and Alexey Solovyev and Enrico Tassi and Laurent Th{\'{e}}ry},
 year         = {2013},
 title        = {A Machine-Checked Proof of the Odd Order Theorem},
 editor       = {Sandrine Blazy and Paulin{-}Mohring, Christine and David Pichardie},
 booktitle    = {{ITP} 2013},
 series       = {LNCS},
 volume       = {7998},
 publisher    = {Springer},
 pages        = {163--179},
 doi          = {10.1007/978-3-642-39634-2\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em14},
)
@inproceedings(DBLP:conf/osdi/GuSCWKSC16,
 author       = {Ronghui Gu and Zhong Shao and Hao Chen and Xiongnan (Newman) Wu and Jieung Kim and Vilhelm Sj{\"{o}}berg and David Costanzo},
 year         = {2016},
 title        = {CertiKOS: An Extensible Architecture for Building Certified Concurrent {OS} Kernels},
 editor       = {Kimberly Keeton and Timothy Roscoe},
 booktitle    = {12th {USENIX} Symposium on Operating Systems Design and Implementation, {OSDI} 2016, Savannah, GA, USA, November 2-4, 2016},
 publisher    = {{USENIX} Association},
 pages        = {653--669},
 doi          = {10.5555/3026877.3026928},
)
@inproceedings(gueneau-hal-02167236,
 author       = {Arma{\"e}l Gu{\'e}neau and Jacques-Henri Jourdan and Arthur Chargu{\'e}raud and Fran{\c c}ois Pottier},
 year         = {2019},
 title        = {{Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}},
 booktitle    = {{ITP 2019 - 10th Conference on Interactive Theorem Proving}},
 address      = {Portland, United States},
)
@article(DBLP:journals/corr/HalesABDHHKMMNNNOPRSTTTUVZ15,
 author       = {Thomas C. 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 M. 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},
 title        = {A formal proof of the Kepler conjecture},
 journal      = {CoRR},
 volume       = {abs/1501.02155},
)
@inproceedings(harrison-holhol,
 author       = {John Harrison},
 year         = {2006},
 title        = {Towards self-verification of HOL Light},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Proceedings of the third International Joint Conference, IJCAR 2006},
 series       = {LNCS},
 volume       = {4130},
 publisher    = {Springer-Verlag},
 address      = {Seattle, WA},
 pages        = {177--191},
)
@article(HerbelinUniverses,
 author       = {Hugo Herbelin},
 year         = {2005},
 title        = {{Type Inference with Algebraic Universes in the Calculus of Inductive Constructions}},
 note         = {Manuscript},
)
@article(Huber:2019uf,
 author       = {Simon Huber},
 year         = {2019},
 title        = {Canonicity for Cubical Type Theory},
 journal      = {Journal of Automated Reasoning},
 volume       = {63},
 number       = {2},
 pages        = {173--210},
 doi          = {10.1007/s10817-018-9469-1},
)
@inproceedings(conf/lics/JaberLPST16,
 author       = {Guilhem Jaber and Gabriel Lewertowski and Pierre{-}Marie P{\'{e}}drot and Matthieu Sozeau and Nicolas Tabareau},
 year         = {2016},
 title        = {The Definitional Side of the Forcing},
 editor       = {Martin Grohe and Eric Koskinen and Natarajan Shankar},
 booktitle    = {{LICS} '16},
 publisher    = {{ACM}},
 pages        = {367--376},
 doi          = {10.1145/2933575.2935320},
)
@article(DBLP:journals/cacm/JungJKD21,
 author       = {Ralf Jung and Jacques{-}Henri Jourdan and Robbert Krebbers and Derek Dreyer},
 year         = {2021},
 title        = {Safe systems programming in Rust},
 journal      = {Commun. {ACM}},
 volume       = {64},
 number       = {4},
 pages        = {144--152},
 doi          = {10.1145/3418295},
)
@article(journals/pacmpl/KaiserZKRD18,
 author       = {Jan{-}Oliver Kaiser and Beta Ziliani and Robbert Krebbers and R{\'{e}}gis{-}Gianas, Yann and Derek Dreyer},
 year         = {2018},
 title        = {Mtac2: typed tactics for backward reasoning in Coq},
 journal      = {{PACMPL}},
 volume       = {2},
 number       = {{ICFP}},
 pages        = {78:1--78:31},
 doi          = {10.1145/3236773},
)
@inproceedings(DBLP:conf/sosp/KleinEHACDEEKNSTW09,
 author       = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas Sewell and Harvey Tuch and Simon Winwood},
 year         = {2009},
 title        = {seL4: formal verification of an OS kernel},
 editor       = {Jeanna Neefe Matthews and Thomas E. Anderson},
 booktitle    = {SOSP},
 publisher    = {ACM},
 pages        = {207--220},
 doi          = {10.1145/1629575.1629596},
)
@article(DBLP:journals/jar/KumarAMO16,
 author       = {Ramana Kumar and Rob Arthan and Magnus O. Myreen and Scott Owens},
 year         = {2016},
 title        = {Self-Formalisation of Higher-Order Logic - Semantics, Soundness, and a Verified Implementation},
 journal      = {J. Autom. Reason.},
 volume       = {56},
 number       = {3},
 pages        = {221--259},
 doi          = {10.1007/s10817-015-9357-x},
)
@inproceedings(conf/itp/Lennon-Bertrand21,
 author       = {Lennon{-}Bertrand, Meven},
 year         = {2021},
 title        = {Complete Bidirectional Typing for the Calculus of Inductive Constructions},
 editor       = {Liron Cohen and Cezary Kaliszyk},
 booktitle    = {{ITP} 2021},
 series       = {LIPIcs},
 volume       = {193},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {24:1--24:19},
 doi          = {10.4230/LIPIcs.ITP.2021.24},
)
@inproceedings(Leroy-compcert-06,
 author       = {Xavier Leroy},
 year         = {2006},
 title        = {Formal certification of a compiler back-end, or: programming a compiler with a proof assistant},
 booktitle    = {33rd symposium Principles of Programming Languages},
 publisher    = {ACM Press},
 pages        = {42--54},
)
@inproceedings(conf/types/Letouzey02,
 author       = {Pierre Letouzey},
 year         = {2002},
 title        = {A {N}ew {E}xtraction for {C}oq.},
 editor       = {Herman Geuvers and Freek Wiedijk},
 booktitle    = {TYPES'02},
 series       = {LNCS},
 volume       = {2646},
 publisher    = {Springer},
 pages        = {200--219},
)
@phdthesis(LetouzeyPhd,
 author       = {Pierre Letouzey},
 year         = {2004},
 title        = {Programmation fonctionnelle certifi{\'e}e: l'extraction de programmes dans l'assistant {Coq}},
 type         = {Th{\`e}se de doctorat},
 school       = {Universit{\'e} Paris-Sud},
)
@inproceedings(10.1145/3314221.3314622,
 author       = {Andreas L\"{o}\"{o}w and Ramana Kumar and Yong Kiam Tan and Magnus O. Myreen and Michael Norrish and Oskar Abrahamsson and Anthony Fox},
 year         = {2019},
 title        = {Verified Compilation on a Verified Processor},
 booktitle    = {PLDI 2019},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {1041--1053},
 doi          = {10.1145/3314221.3314622},
)
@phdthesis(malecha2015thesis,
 author       = {Gregory Michael Malecha},
 year         = {2014},
 title        = {Extensible Proof Engineering in Intensional Type Theory},
 school       = {Harvard University},
)
@inproceedings(paulinTLCA93,
 author       = {Paulin-Mohring, Christine},
 year         = {1993},
 title        = {{I}nductive {D}efinitions in the {S}ystem {Coq} - {R}ules and {P}roperties},
 editor       = {Marc Bezem and Jan Friso Groote},
 booktitle    = {Typed Lambda Calculi and Applications},
 doi          = {10.1007/BFb0037116},
)
@inproceedings(DBLP:conf/lics/PedrotT17,
 author       = {Pierre{-}Marie P{\'{e}}drot and Nicolas Tabareau},
 year         = {2017},
 title        = {An effectful way to eliminate addiction to dependence},
 booktitle    = {{LICS} 2017},
 publisher    = {{IEEE} Computer Society},
 pages        = {1--12},
 doi          = {10.1109/LICS.2017.8005113},
)
@article(DBLP:journals/pacmpl/PedrotT20,
 author       = {Pierre{-}Marie P{\'{e}}drot and Nicolas Tabareau},
 year         = {2020},
 title        = {The fire triangle: how to mix substitution, dependent elimination, and effects},
 journal      = {Proc. {ACM} Program. Lang.},
 volume       = {4},
 number       = {{POPL}},
 pages        = {58:1--58:28},
 doi          = {10.1145/3371126},
)
@inproceedings(DBLP-conf/itp/SchaferTS15,
 author       = {Steven Sch{\"{a}}fer and Tobias Tebbi and Gert Smolka},
 year         = {2015},
 title        = {Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions},
 editor       = {Christian Urban and Xingyuan Zhang},
 booktitle    = {{ITP} 2015},
 series       = {LNCS},
 volume       = {9236},
 publisher    = {Springer},
 pages        = {359--374},
 doi          = {10.1007/978-3-319-22102-1\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em24},
)
@article(journals/jfp/SilesH12,
 author       = {Vincent Siles and Hugo Herbelin},
 year         = {2012},
 title        = {Pure Type System conversion is always typable},
 journal      = {J. Funct. Program.},
 volume       = {22},
 number       = {2},
 pages        = {153--180},
 doi          = {10.1017/S0956796812000044},
)
@inproceedings(sozeau.Coq/Russell/article,
 author       = {Matthieu Sozeau},
 year         = {2007},
 title        = {{Subset Coercions in Coq}},
 editor       = {Thorsten Altenkirch and Conor McBride},
 booktitle    = {TYPES'06},
 series       = {LNCS},
 volume       = {4502},
 publisher    = {Springer},
 pages        = {237--252},
 doi          = {10.1007/978-3-540-74464-1_16},
)
@article(metacoqproject,
 author       = {Matthieu Sozeau and Abhishek Anand and Simon Boulier and Cyril Cohen and Yannick Forster and Fabian Kunze and Gregory Malecha and Nicolas Tabareau and Th{\'e}o Winterhalter},
 year         = {2020},
 title        = {The MetaCoq Project},
 journal      = {Journal of Automated Reasoning},
 volume       = {64},
 number       = {5},
 pages        = {947--999},
 doi          = {10.1007/s10817-019-09540-0},
)
@article(coqcoqcorrect,
 author       = {Matthieu Sozeau and Simon Boulier and Yannick Forster and Nicolas Tabareau and Th{\'e}o Winterhalter},
 year         = {2020},
 title        = {{Coq Coq Correct! Verifying Typechecking and Erasure for Coq, in Coq}},
 journal      = {{Proceedings of the ACM on Programming Languages}},
 volume       = {4},
 number       = {POPL},
 doi          = {10.1145/3371076},
)
@inproceedings(DBLP-conf/itp/SozeauT14,
 author       = {Matthieu Sozeau and Nicolas Tabareau},
 year         = {2014},
 title        = {{Universe Polymorphism in Coq}},
 editor       = {Gerwin Klein and Ruben Gamboa},
 booktitle    = {{ITP} 2014},
 series       = {LNCS},
 volume       = {8558},
 publisher    = {Springer},
 pages        = {499--514},
 doi          = {10.1007/978-3-319-08970-6_32},
)
@inproceedings(DBLP-conf/cpp/StarkSK19,
 author       = {Kathrin Stark and Steven Sch{\"{a}}fer and Jonas Kaiser},
 year         = {2019},
 title        = {Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions},
 editor       = {Assia Mahboubi and Magnus O. Myreen},
 booktitle    = {{CPP} 2019},
 publisher    = {{ACM}},
 pages        = {166--180},
 doi          = {10.1145/3293880.3294101},
)
@article(DBLP:journals/corr/abs-2101-11479,
 author       = {Jonathan Sterling and Carlo Angiuli},
 year         = {2021},
 title        = {Normalization for Cubical Type Theory},
 journal      = {CoRR},
 volume       = {abs/2101.11479},
)
@article(journals/iandc/Takahashi95,
 author       = {Masako Takahashi},
 year         = {1995},
 title        = {Parallel Reductions in lambda-Calculus},
 journal      = {Inf. Comput.},
 volume       = {118},
 number       = {1},
 pages        = {120--127},
 doi          = {10.1006/inco.1995.1057},
)
@article(DBLP:journals/jfp/TanMKFON19,
 author       = {Yong Kiam Tan and Magnus O. Myreen and Ramana Kumar and Anthony C. J. Fox and Scott Owens and Michael Norrish},
 year         = {2019},
 title        = {The verified CakeML compiler backend},
 journal      = {J. Funct. Program.},
 volume       = {29},
 pages        = {e2},
 doi          = {10.1017/S0956796818000229},
)
@misc(coq813,
 author       = {The Coq Development Team},
 year         = {2021},
 title        = {The Coq Proof Assistant},
 doi          = {10.5281/zenodo.4501022},
)
@techreport(timany.hal-01615123,
 author       = {Amin Timany and Matthieu Sozeau},
 year         = {2017},
 title        = {{Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)}},
 type         = {Research Report},
 number       = {RR-9105},
 institution  = {{KU Leuven, Belgium ; Inria Paris}},
)
@inproceedings(DBLP.conf/rta/TimanyS18,
 author       = {Amin Timany and Matthieu Sozeau},
 year         = {2018},
 title        = {Cumulative Inductive Types In Coq},
 editor       = {H{\'{e}}l{\`{e}}ne Kirchner},
 booktitle    = {{FSCD}},
 series       = {LIPIcs},
 volume       = {108},
 pages        = {29:1--29:16},
 doi          = {10.4230/LIPIcs.FSCD.2018.29},
)
@inproceedings(wernerTACS97,
 author       = {Benjamin Werner},
 year         = {1997},
 title        = {Sets in types, types in sets},
 editor       = {Mart{\'\i}n Abadi and Takayasu Ito},
 booktitle    = {Theoretical Aspects of Computer Software},
 publisher    = {Springer},
 pages        = {530--546},
 doi          = {10.1007/BFb0014566},
)
@phdthesis(winte2020,
 author       = {Th{\'e}o Winterhalter},
 year         = {2020},
 title        = {Formalisation and Meta-Theory of Type Theory},
 school       = {{Universit{\'e} de Nantes}},
 note         = {2020NANT4012},
)