@article(1991:explicit-substitutions, author = {M. Abadi and L. Cardelli and P.-L. Curien and J.-J. Lévy}, year = {1991}, title = {Explicit substitutions}, journal = {Journal of Functional Programming}, volume = {1}, number = {4}, pages = {375–416}, doi = {10.1017/S0956796800000186}, ) @inproceedings(2022:ahrens-category-typed-syntax, author = {Benedikt Ahrens and Ralph Matthes and Anders M\"{o}rtberg}, year = {2022}, title = {Implementing a Category-Theoretic Framework for Typed Abstract Syntax}, booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs}, series = {CPP 2022}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, pages = {307–323}, doi = {10.1145/3497775.3503678}, ) @inproceedings(2017:type-scope-safe-programs, author = {Guillaume Allais and James Chapman and Conor McBride and James McKinna}, year = {2017}, title = {Type-and-Scope Safe Programs and Their Proofs}, booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs}, series = {CPP 2017}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, pages = {195–207}, doi = {10.1145/3018610.3018613}, ) @inproceedings(1999:monadic-lambda, author = {Thorsten Altenkirch and Bernhard Reus}, year = {1999}, title = {Monadic Presentations of Lambda Terms Using Generalized Inductive Types}, booktitle = {Proceedings of the 13th International Workshop and 8th Annual Conference of the EACSL on Computer Science Logic}, series = {CSL '99}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, pages = {453–468}, doi = {10.1007/3-540-48168-0_32}, ) @techreport(2010:lngen, author = {Brian Aydemir and Stephanie Weirich}, year = {2010}, title = {{LNgen: Tool Support for Locally Nameless Representations}}, type = {Technical Report}, institution = {{University of Pennsylvania, Department of Computer and Information Science}}, url = {https://repository.upenn.edu/handle/20.500.14332/7902}, ) @inproceedings(2005:poplmark, author = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn and J. Nathan Foster and Benjamin C. Pierce and Peter Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich and Steve Zdancewic}, year = {2005}, title = {Mechanized Metatheory for the Masses: The PoplMark Challenge}, booktitle = {Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics}, series = {TPHOLs'05}, publisher = {Springer-Verlag}, address = {Berlin, Heidelberg}, pages = {50–65}, doi = {10.1007/11541868_4}, ) @mastersthesis(2007:bakkehopfalgebras, author = {Tørris Koløen Bakke}, year = {2007}, title = {Hopf Algebras and Monoidal Categories}, school = {University of Tromsø}, url = {https://munin.uit.no/bitstream/handle/10037/1084/finalthesis.pdf}, ) @article(1994:bh-formal-monads, author = {Fran\c{c}oise Bellegarde and James Hook}, year = {1994}, title = {Substitution: A Formal Methods Case Study Using Monads and Transformations}, journal = {Sci. Comput. Program.}, volume = {23}, number = {2–3}, pages = {287–311}, doi = {10.1016/0167-6423(94)00022-0}, ) @inproceedings(1998:bird-nested, author = {Richard Bird and Lambert Meertens}, year = {1998}, title = {Nested datatypes}, booktitle = {In MPC’98, volume 1422 of LNCS}, publisher = {Springer-Verlag}, pages = {52--67}, doi = {10.1007/BFb0054285}, ) @article(2000:deBruijnNested, author = {Richard Bird and Ross Paterson}, year = {1999}, title = {de Bruijn notation as a nested datatype}, journal = {Journal of Functional Programming}, volume = {9}, pages = {77 -- 91}, doi = {10.1017/S0956796899003366}, ) @article(1969:burstall-struct-rec, author = {R. M. Burstall}, year = {1969}, title = {{Proving Properties of Programs by Structural Induction}}, journal = {The Computer Journal}, volume = {12}, number = {1}, pages = {41--48}, doi = {10.1093/comjnl/12.1.41}, ) @inproceedings(2008:phoas, author = {Adam Chlipala}, year = {2008}, title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics}, booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming}, series = {ICFP '08}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, pages = {143–156}, doi = {10.1145/1411204.1411226}, ) @article(1972:debruijn-dummies, author = {{de Bruijn}, N.G}, year = {1972}, title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem}, journal = {Indagationes Mathematicae (Proceedings)}, volume = {75}, number = {5}, pages = {381--392}, doi = {10.1016/1385-7258(72)90034-0}, ) @inproceedings(2000:ltac, author = {David Delahaye}, year = {2000}, title = {A Tactic Language for the System Coq}, editor = {Michel Parigot and Andrei Voronkov}, booktitle = {Logic for Programming and Automated Reasoning}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, pages = {85--95}, doi = {10.1007/3-540-44404-1_7}, ) @inproceedings(2023:tealeaves, author = {Lawrence Dunn and Val Tannen and Steve Zdancewic}, year = {2023}, title = {{Tealeaves: Structured Monads for Generic First-Order Abstract Syntax Infrastructure}}, editor = {Adam Naumowicz and Ren\'{e} Thiemann}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {268}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, pages = {14:1--14:20}, doi = {10.4230/LIPIcs.ITP.2023.14}, ) @inproceedings(1999:abstractsyntax, author = {M. Fiore and G. Plotkin and D. Turi}, year = {1999}, title = {Abstract syntax and variable binding}, booktitle = {Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158)}, pages = {193--202}, doi = {10.1109/LICS.1999.782615}, ) @inproceedings(2008:fiore-soas, author = {Marcelo Fiore}, year = {2008}, title = {Second-Order and Dependently-Sorted Abstract Syntax}, booktitle = {Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science}, series = {LICS '08}, publisher = {IEEE Computer Society}, address = {USA}, pages = {57–68}, doi = {10.1109/LICS.2008.38}, ) @article(2022:fiore-metatheory-soas, author = {Marcelo Fiore and Dmitrij Szamozvancev}, year = {2022}, title = {Formal Metatheory of Second-Order Abstract Syntax}, journal = {Proc. ACM Program. Lang.}, volume = {6}, number = {POPL}, doi = {10.1145/3498715}, ) @book(fong2018seven, author = {Brendan Fong and David I Spivak}, year = {2018}, title = {Seven Sketches in Compositionality: An Invitation to Applied Category Theory}, doi = {10.48550/arXiv.1803.05316}, ) @article(2002:new-abstract-syntax, author = {Murdoch J. Gabbay and Andrew M. Pitts}, year = {2002}, title = {A New Approach to Abstract Syntax with Variable Binding}, journal = {Form. Asp. Comput.}, volume = {13}, number = {3–5}, pages = {341–363}, doi = {10.1007/s001650200016}, ) @article(2009:essenseiteratorpattern, author = {Jeremy Gibbons and Bruno Oliveira}, year = {2009}, title = {The essence of the Iterator pattern}, journal = {J. Funct. Program.}, volume = {19}, pages = {377--402}, doi = {10.1017/S0956796809007291}, ) @book(hinzemarsden2023, author = {Ralf Hinze and Dan Marsden}, year = {2023}, title = {Introducing String Diagrams: The Art of Category Theory}, publisher = {Cambridge University Press}, doi = {10.1017/9781009317825}, ) @article(2012:traversals, author = {Mauro Jaskelioff and Ondrej Rypacek}, year = {2012}, title = {An Investigation of the Laws of Traversals}, journal = {Electronic Proceedings in Theoretical Computer Science}, volume = {76}, doi = {10.4204/EPTCS.76.5}, ) @inproceedings(2014:cakeml, author = {Ramana Kumar and Magnus O. Myreen and Michael Norrish and Scott Owens}, year = {2014}, title = {CakeML: a verified implementation of {ML}}, booktitle = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014}, pages = {179--192}, doi = {10.1145/2535838.2535841}, ) @inproceedings(2011:GMeta, 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}, publisher = {Springer Berlin Heidelberg}, address = {Berlin, Heidelberg}, pages = {436--455}, doi = {10.1007/978-3-642-28869-2_22}, ) @book(Manes1976, author = {Ernest G. Manes}, year = {1976}, title = {Algebraic Theories}, publisher = {Springer New York}, doi = {10.1007/978-1-4612-9860-1}, ) @unpublished(2005:mcbride, author = {Conor McBride}, year = {2005}, title = {Type-Preserving Renaming and Substitution}, note = {Unpublished note}, ) @article(2008:applicativeprogramming, author = {Conor McBride and Ross Paterson}, year = {2008}, title = {Applicative Programming with Effects}, journal = {J. Funct. Program.}, volume = {18}, number = {1}, pages = {1–13}, doi = {10.1017/S0956796807006326}, ) @inproceedings(1988:moggi-monads, author = {Eugenio Moggi}, year = {1988}, title = {Computational Lambda-Calculus and Monads}, publisher = {IEEE Computer Society Press}, pages = {14--23}, doi = {10.1109/LICS.1989.39155}, ) @inproceedings(1988:hoas, author = {Frank Pfenning and Conal Elliott}, year = {1988}, title = {Higher-Order Abstract Syntax}, volume = {23}, pages = {199--208}, doi = {10.1145/960116.54010}, ) @inproceedings(2003:power-unified-binding, author = {John Power}, year = {2003}, title = {A Unified Category Theoretic Approach to Variable Binding}, booktitle = {Proceedings of the 2003 ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding}, series = {MERLIN '03}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, pages = {1–9}, doi = {10.1145/976571.976578}, ) @article(2008:power-tanaka-typed-signatures, author = {John Power and Miki Tanaka}, year = {2008}, title = {Category Theoretic Semantics for Typed Binding Signatures with Recursion}, journal = {Fundam. Informaticae}, volume = {84}, pages = {221--240}, url = {http://content.iospress.com/articles/fundamenta-informaticae/fi84-2-05}, ) @inproceedings(2015:de-bruijn-algebra-coq, author = {Steven Sch\"{a}fer and Gert Smolka and Tobias Tebbi}, year = {2015}, title = {Completeness and Decidability of de Bruijn Substitution Algebra in Coq}, booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs}, series = {CPP '15}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, pages = {67–73}, doi = {10.1145/2676724.2693163}, ) @inproceedings(2015autosubst, author = {Steven Schäfer and Tobias Tebbi and Gert Smolka}, year = {2015}, title = {Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions}, editor = {Xingyuan Zhang and Christian Urban}, booktitle = {Interactive Theorem Proving - 6th International Conference, {ITP} 2015, Nanjing, China, August 24-27, 2015}, series = {LNAI}, publisher = {Springer-Verlag}, doi = {10.1007/978-3-319-22102-1_24}, ) @inproceedings(2019:autosubst2, 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}, booktitle = {Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs}, series = {CPP 2019}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, pages = {166–180}, doi = {10.1145/3293880.3294101}, ) @(2023:coq, author = {The Coq Development Team}, year = {2023}, title = {The Coq Proof Assistant}, doi = {10.5281/zenodo.8161141}, ) @article(2008:comonadic-computation, author = {Tarmo Uustalu and Varmo Vene}, year = {2008}, title = {Comonadic Notions of Computation}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {203}, number = {5}, pages = {263--284}, doi = {10.1016/j.entcs.2008.05.029}, note = {Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science (CMCS 2008)}, ) @mastersthesis(2019:cofree-traversables, author = {Love Waern}, year = {2019}, title = {Cofree Traversable Functors}, type = {Bachelor's thesis}, url = {https://uu.diva-portal.org/smash/record.jsf?pid=diva2:1369180}, ) @inproceedings(2012:vellvm, author = {Jianzhou Zhao and Santosh Nagarakatte and Milo M.K. Martin and Steve Zdancewic}, year = {2012}, title = {Formalizing the LLVM Intermediate Representation for Verified Program Transformations}, booktitle = {Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, series = {POPL '12}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, pages = {427–440}, doi = {10.1145/2103656.2103709}, )