References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. Tørris Koløen Bakke (2007): Hopf Algebras and Monoidal Categories. University of Tromsø. Available at https://munin.uit.no/bitstream/handle/10037/1084/finalthesis.pdf.
  8. 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.
  9. Richard Bird & Lambert Meertens (1998): Nested datatypes. In: In MPC’98, volume 1422 of LNCS. Springer-Verlag, pp. 52–67, doi:10.1007/BFb0054285.
  10. Richard Bird & Ross Paterson (1999): de Bruijn notation as a nested datatype. Journal of Functional Programming 9, pp. 77 – 91, doi:10.1017/S0956796899003366.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. Marcelo Fiore & Dmitrij Szamozvancev (2022): Formal Metatheory of Second-Order Abstract Syntax. Proc. ACM Program. Lang. 6(POPL), doi:10.1145/3498715.
  19. Brendan Fong & David I Spivak (2018): Seven Sketches in Compositionality: An Invitation to Applied Category Theory, doi:10.48550/arXiv.1803.05316.
  20. 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.
  21. Jeremy Gibbons & Bruno Oliveira (2009): The essence of the Iterator pattern. J. Funct. Program. 19, pp. 377–402, doi:10.1017/S0956796809007291.
  22. Ralf Hinze & Dan Marsden (2023): Introducing String Diagrams: The Art of Category Theory. Cambridge University Press, doi:10.1017/9781009317825.
  23. 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.
  24. 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.
  25. 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.
  26. Ernest G. Manes (1976): Algebraic Theories. Springer New York, doi:10.1007/978-1-4612-9860-1.
  27. Conor McBride (2005): Type-Preserving Renaming and Substitution. Unpublished note.
  28. Conor McBride & Ross Paterson (2008): Applicative Programming with Effects. J. Funct. Program. 18(1), pp. 1–13, doi:10.1017/S0956796807006326.
  29. Eugenio Moggi (1988): Computational Lambda-Calculus and Monads. IEEE Computer Society Press, pp. 14–23, doi:10.1109/LICS.1989.39155.
  30. Frank Pfenning & Conal Elliott (1988): Higher-Order Abstract Syntax 23, pp. 199–208, doi:10.1145/960116.54010.
  31. 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.
  32. John Power & Miki Tanaka (2008): Category Theoretic Semantics for Typed Binding Signatures with Recursion. Fundam. Informaticae 84, pp. 221–240. Available at http://content.iospress.com/articles/fundamenta-informaticae/fi84-2-05.
  33. 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.
  34. 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.
  35. 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.
  36. The Coq Development Team (2023): The Coq Proof Assistant, doi:10.5281/zenodo.8161141.
  37. 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).
  38. Love Waern (2019): Cofree Traversable Functors. Bachelor's thesis. Available at https://uu.diva-portal.org/smash/record.jsf?pid=diva2:1369180.
  39. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org