References

• [appel2007compiling]: Compiling with continuations Andrew W Appel. Compiling with continuations. Cambridge university press, 2007.
• [baader1998term]: Term rewriting and all that Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1998.
• [cardone2006history]: History of lambda-calculus and combinatory logic Felice Cardone and J Roger Hindley. History of lambda-calculus and combinatory logic. Handbook of the History of Logic, 5:723–817, 2006.
• [coq1992paradox]: The paradox of trees in type theory Thierry Coquand. The paradox of trees in type theory. BIT, 32:10–14, 03 1992. doi:10.1007/BF01995104.
• [girard1989proofs]: Proofs and types Jean-Yves Girard, Paul Taylor, and Yves Lafont. Proofs and types. Volume 7. Cambridge university press Cambridge, 1989.
• [Pierce:SF1]: Logical Foundations Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, and Brent Yorgey. Logical Foundations. Volume 1 of Software Foundations. Electronic textbook, 2025. URL: http://softwarefoundations.cis.upenn.edu.
• [plfa22_08]: Programming Language Foundations in {A}gda Philip Wadler, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Online, August 2022. URL: https://plfa.inf.ed.ac.uk/22.08/.
• [pugh1991omega]: The Omega test: a fast and practical integer programming algorithm for dependence analysis William Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. In Proceedings of the 1991 ACM/IEEE conference on Supercomputing, 4–13. 1991.
• [rijke2022introduction]: Introduction to homotopy type theory Egbert Rijke. Introduction to homotopy type theory. arXiv preprint arXiv:2212.11082, 2022.
• [simmons2011introduction]: An introduction to category theory Harold Simmons. An introduction to category theory. Cambridge University Press, 2011.
• [sorensen2006lectures]: Lectures on the Curry-Howard isomorphism Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Volume 149. Elsevier, 2006.
• [statman1979intuitionistic]: Intuitionistic propositional logic is polynomial-space complete Richard Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9(1):67–72, 1979.
• [vene2000categorical]: Categorical programming with inductive and coinductive types Varmo Vene. Categorical programming with inductive and coinductive types. Citeseer, 2000.