@misc(HOLlibrary,
 author       = {Jasmin Blanchette Alexander Krauss, Brian Huffman},
 title        = {This is a library of Countable Theory in {Isabelle}/{HOL}},
 howpublished = {\url{https://devel.isa-afp.org/browser_info/current/HOL/HOL-Library/Countable.html}},
)
@article(coqPL2020,
 author       = {A. A. de Amorim},
 year         = {2020},
 title        = {Deriving Instances with Dependent Types},
 journal      = {CoqPL 2020},
)
@inproceedings(anand2014generic,
 author       = {Abhishek Anand and Vincent Rahli},
 year         = {2014},
 title        = {A Generic Approach to Proofs about Substitution},
 editor       = {Amy P. Felty and Brigitte Pientka},
 booktitle    = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, {LFMTP} '14, Vienna, Austria, July 17, 2014},
 publisher    = {{ACM}},
 pages        = {5: 1--5: 8},
 doi          = {10.1145/2631172.2631177},
)
@article(aydemir2010lngen,
 author       = {Brian Aydemir and Stephanie Weirich},
 year         = {2010},
 title        = {LNgen: Tool support for locally nameless representations},
)
@article(barras1999coq,
 author       = {Bruno Barras and Samuel Boutin and Cristina Cornes and Judica{\"e}l Courant and Yann Coscoy and David Delahaye and Daniel de Rauglaudre and Jean-Christophe Filli{\^a}tre and Eduardo Gim{\'e}nez and Hugo Herbelin},
 year         = {1999},
 title        = {The {Coq} proof assistant reference manual},
 journal      = {INRIA, version},
 volume       = {6},
 number       = {11},
)
@inproceedings(cao2017bringing,
 author       = {Qinxiang Cao and Santiago Cuellar and Andrew W. Appel},
 year         = {2017},
 title        = {Bringing Order to the Separation Logic Jungle},
 editor       = {Bor{-}Yuh Evan Chang},
 booktitle    = {Programming Languages and Systems - 15th Asian Symposium, {APLAS} 2017, Suzhou, China, November 27-29, 2017, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10695},
 publisher    = {Springer},
 pages        = {190--211},
 doi          = {10.1007/978-3-319-71237-6\_10},
)
@inproceedings(chlipala2008parametric,
 author       = {Adam Chlipala},
 year         = {2008},
 title        = {Parametric higher-order abstract syntax for mechanized semantics},
 editor       = {James Hook and Peter Thiemann},
 booktitle    = {Proceeding of the 13th {ACM} {SIGPLAN} international conference on Functional programming, {ICFP} 2008, Victoria, BC, Canada, September 20-28, 2008},
 publisher    = {{ACM}},
 pages        = {143--156},
 doi          = {10.1145/1411204.1411226},
)
@book(ebbinghaus2013mathematical,
 author       = {Heinz{-}Dieter Ebbinghaus and J{\"{o}}rg Flum and Wolfgang Thomas},
 year         = {1994},
 title        = {Mathematical logic {(2.} ed.)},
 series       = {Undergraduate texts in mathematics},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4757-2355-7},
)
@inproceedings(forster2019synthetic,
 author       = {Yannick Forster and Dominik Kirst and Gert Smolka},
 year         = {2019},
 title        = {On synthetic undecidability in coq, with an application to the entscheidungsproblem},
 editor       = {Assia Mahboubi and Magnus O. Myreen},
 booktitle    = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January 14-15, 2019},
 publisher    = {{ACM}},
 pages        = {38--51},
 doi          = {10.1145/3293880.3294091},
)
@inproceedings(forster2020completeness,
 author       = {Yannick Forster and Dominik Kirst and Dominik Wehr},
 year         = {2020},
 title        = {Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory},
 editor       = {Sergei N. Art{\"{e}}mov and Anil Nerode},
 booktitle    = {Logical Foundations of Computer Science - International Symposium, {LFCS} 2020, Deerfield Beach, FL, USA, January 4-7, 2020, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {11972},
 publisher    = {Springer},
 pages        = {47--74},
 doi          = {10.1007/978-3-030-36755-8\_4},
)
@inproceedings(113772,
 author       = {Peter {Freyd}},
 year         = {1990},
 title        = {Recursive types reduced to inductive types},
 booktitle    = {[1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science},
 pages        = {498--507},
 doi          = {10.1109/LICS.1990.113772},
)
@inproceedings(316071,
 author       = {M. Hofmann and T. Streicher},
 year         = {1994},
 title        = {The groupoid model refutes uniqueness of identity proofs},
 booktitle    = {Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science},
 pages        = {208--212},
 doi          = {10.1109/LICS.1994.316071},
)
@inproceedings(lee2012gm,
 author       = {Gyesik Lee and Bruno C. d. S. Oliveira and Sungkeun Cho and Kwangkeun Yi},
 year         = {2012},
 title        = {GMeta: {A} Generic Formal Metatheory Framework for First-Order Representations},
 editor       = {Helmut Seidl},
 booktitle    = {Programming Languages and Systems - 21st European Symposium on Programming, {ESOP} 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7211},
 publisher    = {Springer},
 pages        = {436--455},
 doi          = {10.1007/978-3-642-28869-2\_22},
)
@inproceedings(DBLP:conf/cade/MouraKADR15,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Soonho Kong and Jeremy Avigad and Floris van Doorn and Jakob von Raumer},
 year         = {2015},
 title        = {The Lean Theorem Prover (System Description)},
 editor       = {Amy P. Felty and Aart Middeldorp},
 booktitle    = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9195},
 publisher    = {Springer},
 pages        = {378--388},
 doi          = {10.1007/978-3-319-21401-6\_26},
)
@book(nederpelt2014type,
 author       = {Rob Nederpelt and Herman Geuvers},
 year         = {2014},
 title        = {Type theory and formal proof: an introduction},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139567725},
)
@incollection(paulin2015introduction,
 author       = {Paulin-Mohring, Christine},
 year         = {2015},
 title        = {{Introduction to the Calculus of Inductive Constructions}},
 editor       = {Bruno Woltzenlogel Paleo and David Delahaye},
 booktitle    = {{All about Proofs, Proofs for All}},
 series       = {Studies in Logic (Mathematical logic and foundations)},
 volume       = {55},
 publisher    = {{College Publications}},
 url          = {https://hal.inria.fr/hal-01094195},
)
@inproceedings(polonowski2013automatically,
 author       = {Emmanuel Polonowski},
 year         = {2013},
 title        = {Automatically Generated Infrastructure for De Bruijn Syntaxes},
 editor       = {Sandrine Blazy and Paulin{-}Mohring, Christine and David Pichardie},
 booktitle    = {Interactive Theorem Proving - 4th International Conference, {ITP} 2013, Rennes, France, July 22-26, 2013. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {7998},
 publisher    = {Springer},
 pages        = {402--417},
 doi          = {10.1007/978-3-642-39634-2\_29},
)
@inproceedings(schafer2015completeness,
 author       = {Steven Sch{\"{a}}fer and Gert Smolka and Tobias Tebbi},
 year         = {2015},
 title        = {Completeness and Decidability of de Bruijn Substitution Algebra in Coq},
 editor       = {Xavier Leroy and Alwen Tiu},
 booktitle    = {Proceedings of the 2015 Conference on Certified Programs and Proofs, {CPP} 2015, Mumbai, India, January 15-17, 2015},
 publisher    = {{ACM}},
 pages        = {67--73},
 doi          = {10.1145/2676724.2693163},
)
@inproceedings(schafer2015autosubst,
 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    = {Interactive Theorem Proving - 6th International Conference, {ITP} 2015, Nanjing, China, August 24-27, 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9236},
 publisher    = {Springer},
 pages        = {359--374},
 doi          = {10.1007/978-3-319-22102-1\_24},
)
@inproceedings(stark2019autosubst,
 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    = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January 14-15, 2019},
 publisher    = {{ACM}},
 pages        = {166--180},
 doi          = {10.1145/3293880.3294101},
)
@article(0Deriving,
 author       = {Christian Sternagel and Ren{\'{e}} Thiemann},
 year         = {2015},
 title        = {Deriving class instances for datatypes},
 journal      = {Arch. Formal Proofs},
 volume       = {2015},
 url          = {https://www.isa-afp.org/entries/Deriving.shtml},
)