M. Abadi, L. Cardelli, P.-L. Curien & J.-J. Lévy (1991):
Explicit substitutions.
Journal of Functional Programming 1(4),
pp. 375–416,
doi:10.1017/S0956796800000186.
Benedikt Ahrens, Ralph Matthes & Anders Mörtberg (2022):
Implementing a Category-Theoretic Framework for Typed Abstract Syntax.
In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs,
CPP 2022.
Association for Computing Machinery,
New York, NY, USA,
pp. 307–323,
doi:10.1145/3497775.3503678.
Guillaume Allais, James Chapman, Conor McBride & James McKinna (2017):
Type-and-Scope Safe Programs and Their Proofs.
In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs,
CPP 2017.
Association for Computing Machinery,
New York, NY, USA,
pp. 195–207,
doi:10.1145/3018610.3018613.
Thorsten Altenkirch & Bernhard Reus (1999):
Monadic Presentations of Lambda Terms Using Generalized Inductive Types.
In: Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic,
CSL '99.
Springer-Verlag,
Berlin, Heidelberg,
pp. 453–468,
doi:10.1007/3-540-48168-0_32.
Brian Aydemir & Stephanie Weirich (2010):
LNgen: Tool Support for Locally Nameless Representations.
Technical Report.
University of Pennsylvania, Department of Computer and Information Science.
Available at https://repository.upenn.edu/handle/20.500.14332/7902.
Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich & Steve Zdancewic (2005):
Mechanized Metatheory for the Masses: The PoplMark Challenge.
In: Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics,
TPHOLs'05.
Springer-Verlag,
Berlin, Heidelberg,
pp. 50–65,
doi:10.1007/11541868_4.
Françoise Bellegarde & James Hook (1994):
Substitution: A Formal Methods Case Study Using Monads and Transformations.
Sci. Comput. Program. 23(2–3),
pp. 287–311,
doi:10.1016/0167-6423(94)00022-0.
Richard Bird & Lambert Meertens (1998):
Nested datatypes.
In: In MPC’98, volume 1422 of LNCS.
Springer-Verlag,
pp. 52–67,
doi:10.1007/BFb0054285.
Richard Bird & Ross Paterson (1999):
de Bruijn notation as a nested datatype.
Journal of Functional Programming 9,
pp. 77 – 91,
doi:10.1017/S0956796899003366.
R. M. Burstall (1969):
Proving Properties of Programs by Structural Induction.
The Computer Journal 12(1),
pp. 41–48,
doi:10.1093/comjnl/12.1.41.
Adam Chlipala (2008):
Parametric Higher-Order Abstract Syntax for Mechanized Semantics.
In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming,
ICFP '08.
Association for Computing Machinery,
New York, NY, USA,
pp. 143–156,
doi:10.1145/1411204.1411226.
N.G de Bruijn (1972):
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem.
Indagationes Mathematicae (Proceedings) 75(5),
pp. 381–392,
doi:10.1016/1385-7258(72)90034-0.
David Delahaye (2000):
A Tactic Language for the System Coq.
In: Michel Parigot & Andrei Voronkov: Logic for Programming and Automated Reasoning.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 85–95,
doi:10.1007/3-540-44404-1_7.
Lawrence Dunn, Val Tannen & Steve Zdancewic (2023):
Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure.
In: Adam Naumowicz & René Thiemann: 14th International Conference on Interactive Theorem Proving (ITP 2023),
Leibniz International Proceedings in Informatics (LIPIcs) 268.
Schloss Dagstuhl – Leibniz-Zentrum für Informatik,
Dagstuhl, Germany,
pp. 14:1–14:20,
doi:10.4230/LIPIcs.ITP.2023.14.
M. Fiore, G. Plotkin & D. Turi (1999):
Abstract syntax and variable binding.
In: Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158),
pp. 193–202,
doi:10.1109/LICS.1999.782615.
Marcelo Fiore (2008):
Second-Order and Dependently-Sorted Abstract Syntax.
In: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science,
LICS '08.
IEEE Computer Society,
USA,
pp. 57–68,
doi:10.1109/LICS.2008.38.
Marcelo Fiore & Dmitrij Szamozvancev (2022):
Formal Metatheory of Second-Order Abstract Syntax.
Proc. ACM Program. Lang. 6(POPL),
doi:10.1145/3498715.
Brendan Fong & David I Spivak (2018):
Seven Sketches in Compositionality: An Invitation to Applied Category Theory,
doi:10.48550/arXiv.1803.05316.
Murdoch J. Gabbay & Andrew M. Pitts (2002):
A New Approach to Abstract Syntax with Variable Binding.
Form. Asp. Comput. 13(3–5),
pp. 341–363,
doi:10.1007/s001650200016.
Jeremy Gibbons & Bruno Oliveira (2009):
The essence of the Iterator pattern.
J. Funct. Program. 19,
pp. 377–402,
doi:10.1017/S0956796809007291.
Ralf Hinze & Dan Marsden (2023):
Introducing String Diagrams: The Art of Category Theory.
Cambridge University Press,
doi:10.1017/9781009317825.
Mauro Jaskelioff & Ondrej Rypacek (2012):
An Investigation of the Laws of Traversals.
Electronic Proceedings in Theoretical Computer Science 76,
doi:10.4204/EPTCS.76.5.
Ramana Kumar, Magnus O. Myreen, Michael Norrish & Scott Owens (2014):
CakeML: a verified implementation of ML.
In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014,
pp. 179–192,
doi:10.1145/2535838.2535841.
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.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 436–455,
doi:10.1007/978-3-642-28869-2_22.
Conor McBride (2005):
Type-Preserving Renaming and Substitution.
Unpublished note.
Conor McBride & Ross Paterson (2008):
Applicative Programming with Effects.
J. Funct. Program. 18(1),
pp. 1–13,
doi:10.1017/S0956796807006326.
Eugenio Moggi (1988):
Computational Lambda-Calculus and Monads.
IEEE Computer Society Press,
pp. 14–23,
doi:10.1109/LICS.1989.39155.
Frank Pfenning & Conal Elliott (1988):
Higher-Order Abstract Syntax 23,
pp. 199–208,
doi:10.1145/960116.54010.
John Power (2003):
A Unified Category Theoretic Approach to Variable Binding.
In: Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding,
MERLIN '03.
Association for Computing Machinery,
New York, NY, USA,
pp. 1–9,
doi:10.1145/976571.976578.
Steven Schäfer, Gert Smolka & Tobias Tebbi (2015):
Completeness and Decidability of de Bruijn Substitution Algebra in Coq.
In: Proceedings of the 2015 Conference on Certified Programs and Proofs,
CPP '15.
Association for Computing Machinery,
New York, NY, USA,
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: Xingyuan Zhang & Christian Urban: Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015,
LNAI.
Springer-Verlag,
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: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs,
CPP 2019.
Association for Computing Machinery,
New York, NY, USA,
pp. 166–180,
doi:10.1145/3293880.3294101.
Tarmo Uustalu & Varmo Vene (2008):
Comonadic Notions of Computation.
Electronic Notes in Theoretical Computer Science 203(5),
pp. 263–284,
doi:10.1016/j.entcs.2008.05.029.
Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science (CMCS 2008).
Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin & Steve Zdancewic (2012):
Formalizing the LLVM Intermediate Representation for Verified Program Transformations.
In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL '12.
Association for Computing Machinery,
New York, NY, USA,
pp. 427–440,
doi:10.1145/2103656.2103709.