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