Lectures onType Theory
Bibliography
bibliography

Bibliography

Abadi, Martín, and Luca Cardelli. 1995. “A Theory of Primitive Objects: Second-Order Systems.” Science of Computer Programming 25 (2–3): 81–116. https://doi.org/10.1016/0167-6423(95)00010-0.
Abadi, Martín, and Luca Cardelli. 1996a. “A Theory of Primitive Objects: Untyped and First-Order Systems.” Information and Computation 125 (2): 78–102. https://doi.org/10.1006/inco.1996.0024.
Abadi, Martín, and Luca Cardelli. 1996b. “On Subtyping and Matching.” ACM Transactions on Programming Languages and Systems 18 (4): 401–23. https://doi.org/10.1145/233561.233563.
Abadi, Martín, Luca Cardelli, and Ramesh Viswanathan. 1996. “An Interpretation of Objects and Object Types.” Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 396–409. https://doi.org/10.1145/237721.237809.
Abbott, Michael, Thorsten Altenkirch, and Neil Ghani. 2005. “Containers: Constructing Strictly Positive Types.” Theoretical Computer Science 342 (1): 3–27. https://doi.org/10.1016/j.tcs.2005.06.002.
Abbott, Michael, Thorsten Altenkirch, Neil Ghani, and Conor McBride. 2003. “Derivatives of Containers.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 2701. https://doi.org/10.1007/3-540-44904-3_2.
Abbott, Michael, Thorsten Altenkirch, Neil Ghani, and Conor McBride. 2005. “$\\partial$ for Data: Differentiating Data Structures.” Fundamenta Informaticae 65 (1–2): 1–28. https://doi.org/10.3233/FUN-2005-651-202.
Abel, Andreas. 1998. foetus—a Termination Checker for Simple Functional Programs. https://andreasabel.github.io/foetus-report/foetus.pdf.
Abel, Andreas. 2013. “Normalization by Evaluation: Dependent Types and Impredicativity.” Habilitation thesis, Ludwig-Maximilians-Universität München.
Abel, Andreas, and Thorsten Altenkirch. 2002. “A Predicative Analysis of Structural Recursion.” Journal of Functional Programming 12 (1): 1–41. https://doi.org/10.1017/S0956796801004191.
Abel, Andreas, and Thierry Coquand. 2020. “Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality.” Logical Methods in Computer Science 16 (2): 14:1–16. https://doi.org/10.23638/LMCS-16(2:14)2020.
Abel, Andreas, Nils Anders Danielsson, and Oskar Eriksson. 2026. A Graded Modal Dependent Type Theory with Erasure, Formalized. https://arxiv.org/abs/2603.29716.
Abel, Andreas, Ralph Matthes, and Tarmo Uustalu. 2005. “Iteration and Coiteration Schemes for Higher-Order and Nested Datatypes.” Theoretical Computer Science 333 (1–2): 3–66. https://doi.org/10.1016/j.tcs.2004.10.017.
Abel, Andreas, Joakim Öhman, and Andrea Vezzosi. 2018. “Decidability of Conversion for Type Theory in Type Theory.” Proceedings of the ACM on Programming Languages 2 (POPL): 23:1–29. https://doi.org/10.1145/3158111.
Abel, Andreas, and Brigitte Pientka. 2013. Wellfounded Recursion with Copatterns and Sized Types.
Abel, Andreas, and Brigitte Pientka. 2016. “Well-Founded Recursion with Copatterns and Sized Types.” Journal of Functional Programming 26: e2. https://doi.org/10.1017/S0956796816000022.
Abel, Andreas, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. “Copatterns: Programming Infinite Structures by Observations.” Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 27–38. https://doi.org/10.1145/2429069.2429075.
Abramsky, Samson. 2003. Course on Game Semantics. https://www.cs.ox.ac.uk/samson.abramsky/gsem/.
Abramsky, Samson, and Achim Jung. 1994. “Domain Theory.” In Handbook of Logic in Computer Science, vol. 3. Oxford University Press. https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf.
Ackerman, Nathanael L., Cameron E. Freer, and Daniel M. Roy. 2019. “On the Computability of Conditional Probability.” Journal of the ACM 66 (3): 23:1–40. https://doi.org/10.1145/3321699.
Aczel, Peter. 1977. “An Introduction to Inductive Definitions.” In Handbook of Mathematical Logic, edited by Jon Barwise, vol. 90. Studies in Logic and the Foundations of Mathematics. North-Holland. https://doi.org/10.1016/S0049-237X(08)71120-0.
Adams, Robin, and Zhaohui Luo. 2010a. “Classical Predicative Logic-Enriched Type Theories.” Annals of Pure and Applied Logic 161 (11): 1315–45. https://doi.org/10.1016/j.apal.2010.04.005.
Adams, Robin, and Zhaohui Luo. 2010b. Formalisation of Weyl’s Predicative Mathematics in Plastic. https://web.archive.org/web/20101205120600/http://www.cs.rhul.ac.uk/~robin/weyl/.
Adams, Robin, and Zhaohui Luo. 2011. “A Pluralist Approach to the Formalisation of Mathematics.” Mathematical Structures in Computer Science 21 (5): 913–42. https://doi.org/10.1017/S0960129511000156.
Adjedj, Arthur, Meven Lennon-Bertrand, Thibaut Benjamin, and Kenji Maillard. 2025. AdapTT: Functoriality for Dependent Type Casts. https://doi.org/10.1145/3776664.
Agda Contributors. 2026. Agda Reflection. https://agda.readthedocs.io/en/latest/language/reflection.html.
Agda Development Team. 2026. Agda: Positivity, Termination, Mutual Recursion, and Coinduction. https://github.com/agda/agda.
Agda Team. 2026a. Lambda Abstraction. Agda Language Reference. https://agda.readthedocs.io/en/stable/language/lambda-abstraction.html.
Agda Team. 2026b. Record Types. Agda Language Reference. https://agda.readthedocs.io/en/latest/language/record-types.html.
Ahman, Danel. 2017. “Fibred Computational Effects.” PhD thesis, University of Edinburgh. https://danel.ahman.ee/papers/phd-thesis.pdf.
Ahman, Danel, Neil Ghani, and Gordon D. Plotkin. 2016. “Dependent Types and Fibred Computational Effects.” Foundations of Software Science and Computation Structures, Lecture notes in computer science, vol. 9634: 36–54. https://doi.org/10.1007/978-3-662-49630-5_3.
Ahman, Danel, Cătălin Hriţcu, Kenji Maillard, et al. 2017. “Dijkstra Monads for Free.” Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/3009837.3009878.
Ahman, Danel, and Gašper Žajdela. 2024. “A Stateful Time-Aware Operational Semantics for Temporal Resources.” Mathematical Structures in Functional Programming.
Ahmed, Amal, Matthew Fluet, and Greg Morrisett. 2007. “L3: A Linear Language with Locations.” Fundamenta Informaticae 77 (4): 397–449.
Ahn, Ki Yung. 2014. “The Nax Language: Unifying Functional Programming and Logical Reasoning in a Language Based on Mendler-Style Recursion Schemes and Term-Indexed Types.” PhD thesis, Portland State University. https://doi.org/10.15760/etd.2086.
Ahn, Ki Yung, and Tim Sheard. 2011. “A Hierarchy of Mendler Style Recursion Combinators: Taming Inductive Datatypes with Negative Occurrences.” Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, 234–46. https://doi.org/10.1145/2034773.2034807.
Ahn, Ki Yung, Tim Sheard, Marcelo Fiore, and Andrew M. Pitts. 2013. “System Fi: A Higher-Order Polymorphic Lambda-Calculus with Erasable Term-Indices.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 7941: 15–30. https://doi.org/10.1007/978-3-642-38946-7_4.
Aiken, Alex. n.d. Objects. https://web.stanford.edu/class/cs242/materials/lectures/lecture10.pdf.
Algehed, Maximilian, and Jean-Philippe Bernardy. 2019. “Simple Noninterference from Parametricity.” Proceedings of the ACM on Programming Languages 3 (ICFP): 1–22. https://doi.org/10.1145/3341693.
Allais, Guillaume, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2021. “A Type- and Scope-Safe Universe of Syntaxes with Binding: Their Semantics and Proofs.” Journal of Functional Programming 31: e22. https://doi.org/10.1017/S0956796820000076.
Allen, Stuart F. 1987b. “A Non-Type-Theoretic Semantics for Type-Theoretic Language.” PhD thesis and Technical Report TR 87-866, Cornell University. https://hdl.handle.net/1813/6706.
Allen, Stuart F. 1987a. “A Non-Type-Theoretic Semantics for Type-Theoretic Language.” PhD thesis and Technical Report TR 87-866, Cornell University. https://hdl.handle.net/1813/6706.
Allen, Stuart F., Mark Bickford, Robert L. Constable, et al. 2006. “Innovations in Computational Type Theory Using Nuprl.” Journal of Applied Logic 4 (4): 428–69. https://doi.org/10.1016/j.jal.2005.10.005.
Altenkirch, Thorsten. 2023. Categories with Families for Simple Types. https://fplunchnott.wordpress.com/2023/05/12/categories-with-families-for-simple-types/.
Altenkirch, Thorsten, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman. 2024. “Internal Parametricity, Without an Interval.” Proceedings of the ACM on Programming Languages 8 (POPL): 2340–69. https://doi.org/10.1145/3632920.
Altenkirch, Thorsten, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. 2015. “Indexed Containers.” Journal of Functional Programming 25: e5. https://doi.org/10.1017/S095679681500009X.
Altenkirch, Thorsten, and Ambrus Kaposi. 2017. “Normalisation by Evaluation for Type Theory, in Type Theory.” Logical Methods in Computer Science 13 (4:1): 1–26. https://doi.org/10.23638/LMCS-13(4:1)2017.
Altenkirch, Thorsten, and Conor McBride. 2006. “Towards Observational Type Theory.” https://personal.cis.strath.ac.uk/conor.mcbride/ott.pdf.
Altenkirch, Thorsten, Conor McBride, and Peter Morris. 2007. “Generic Programming with Dependent Types.” In Datatype-Generic Programming, vol. 4719. Lecture Notes in Computer Science. https://doi.org/10.1007/978-3-540-76786-2_4.
Altenkirch, Thorsten, Conor McBride, and Wouter Swierstra. 2007. “Observational Equality, Now!” Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification (Freiburg, Germany), PLPV ’07, 57–68. https://doi.org/10.1145/1292597.1292608.
Amadio, Roberto M., and Luca Cardelli. 1993. “Subtyping Recursive Types.” ACM Transactions on Programming Languages and Systems 15 (4): 575–631. https://doi.org/10.1145/155183.155231.
Amin, Nada. 2016. “Dependent Object Types.” PhD thesis, EPFL. https://infoscience.epfl.ch/entities/publication/db9ab8c7-0b4a-432a-b619-4c59cbcddc84.
Amin, Nada, and Tiark Rompf. 2018. “Collapsing Towers of Interpreters.” Proceedings of the ACM on Programming Languages 2 (POPL): 52:1–33. https://doi.org/10.1145/3158140.
Anand, Abhishek, and Vincent Rahli. 2014. “Towards a Formally Verified Proof Assistant.” Interactive Theorem Proving, Lecture notes in computer science, vol. 8558: 27–44. https://doi.org/10.1007/978-3-319-08970-6_3.
Andreoli, Jean-Marc. 1992. “Logic Programming with Focusing Proofs in Linear Logic.” Journal of Logic and Computation 2 (3): 297–347. https://doi.org/10.1093/logcom/2.3.297.
Andreoli, Jean-Marc, and Roberto Maieli. 1999. “Focusing and Proof-Nets in Linear and Non-Commutative Logic.” Logic for Programming and Automated Reasoning, Lecture notes in computer science, vol. 1705: 320–36. https://doi.org/10.1007/3-540-48242-3_20.
Angiuli, Carlo. 2019. “Computational Semantics of Cartesian Cubical Type Theory.” PhD Thesis CMU-CS-19-127. Carnegie Mellon University.
Angiuli, Carlo, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, and Daniel R. Licata. 2021. “Syntax and Models of Cartesian Cubical Type Theory.” Mathematical Structures in Computer Science 31 (4): 424–68. https://doi.org/10.1017/S0960129521000347.
Angiuli, Carlo, and Daniel Gratzer. 2026. Principles of Dependent Type Theory. Cambridge University Press. https://www.danielgratzer.com/papers/type-theory-book.pdf.
Annenkov, Danil, Mikkel Milo, Jakob Botsch Nielsen, and Bas Spitters. 2022. “Extracting Functional Programs from Coq, in Coq.” Journal of Functional Programming, ahead of print. https://doi.org/10.1017/S0956796822000077.
Appel, Andrew W. 2001. “Foundational Proof-Carrying Code.” Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 247–56. https://doi.org/10.1109/LICS.2001.932501.
Asperti, Andrea, and Giuseppe Longo. 1991. Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press.
Asperti, Andrea, and Harry G. Mairson. 2001. “Parallel Beta Reduction Is Not Elementary Recursive.” Information and Computation 170 (1): 49–80. https://doi.org/10.1006/inco.2001.2869.
Asperti, Andrea, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2009. “A Compact Kernel for the Calculus of Inductive Constructions.” Sādhanā 34 (1). https://doi.org/10.1007/s12046-009-0003-3.
Atkey, Robert. 2018. “Syntax and Semantics of Quantitative Type Theory.” Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 56–65. https://doi.org/10.1145/3209108.3209189.
Atkey, Robert, and Conor McBride. 2013. “Productive Coprogramming with Guarded Recursion.” Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, 197–208. https://doi.org/10.1145/2500365.2500597.
Aubert, Clément. 2017. Reversible Computation. Classroom presentation at Appalachian State University. https://aubert.perso.math.cnrs.fr/notes/exemples_cand_tt/ASU/cp.html.
Avigad, Jeremy, and Solomon Feferman. 1998. “Gödel’s Functional (Dialectica) Interpretation.” In Handbook of Proof Theory, edited by Samuel R. Buss, vol. 137. Studies in Logic and the Foundations of Mathematics. https://doi.org/10.1016/S0049-237X(98)80020-7.
Awodey, Steve. 2018. “Natural Models of Homotopy Type Theory.” Mathematical Structures in Computer Science 28 (2): 241–86. https://doi.org/10.1017/S0960129516000268.
Awodey, Steve. 2024. Introduction to Categorical Logic. https://awodey.github.io/catlog/.
Awodey, Steve. 2025. Notes on Type Theory. https://awodey.github.io/typetheory/.
Awodey, Steven, and Andrej Bauer. 2004. “Propositions as [Types].” Journal of Logic and Computation 14 (4): 447–71. https://doi.org/10.1093/logcom/14.4.447.
Aydemir, Brian E., Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. 2008. “Engineering Formal Metatheory.” Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2008), 3–15. https://doi.org/10.1145/1328438.1328443.
Baader, Franz, and Wayne Snyder. 2001. “Unification Theory.” In Handbook of Automated Reasoning, edited by Alan Robinson and Andrei Voronkov, vol. 1. Elsevier; MIT Press. https://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf.
Baez, John C., and Mike Stay. 2009. Physics, Topology, Logic and Computation: A Rosetta Stone. https://arxiv.org/abs/0903.0340.
Bahr, Patrick, Christian Uldal Graulund, and Rasmus Ejlers Møgelberg. 2019. “Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming Without Space Leaks.” Proceedings of the ACM on Programming Languages 3 (ICFP): 109:1–27. https://doi.org/10.1145/3341713.
Baillot, Patrick, and Virgile Mogbil. 2004. “Soft Lambda-Calculus: A Language for Polynomial Time Computation.” Foundations of Software Science and Computation Structures. https://doi.org/10.1007/978-3-540-24727-2_4.
Barbanera, Franco, Mariangiola Dezani-Ciancaglini, and Ugo de’Liguoro. 1995. “Intersection and Union Types: Syntax and Semantics.” Information and Computation 119 (2): 202–30. https://doi.org/10.1006/inco.1995.1086.
Barbarossa, Davide, and Giulio Guerrieri. 2025. The Lambda-Calculus, from Minimal to Classical Logic. https://davidebarbarossa12.github.io/Enseignements/2024-25/ESSLLI.html.
Barendregt, Henk P. 1991. “An Introduction to Generalized Type Systems.” Journal of Functional Programming 1 (2): 125–54. https://doi.org/10.1017/S0956796800020025.
Barendregt, Henk P. 1992. “Lambda Calculi with Types.” In Handbook of Logic in Computer Science, edited by Samson Abramsky, Dov M. Gabbay, and Tom S. E. Maibaum, vol. 2. Oxford University Press.
Barendsen, Erik, and Sjaak Smetsers. 1996. “Uniqueness Typing for Functional Languages with Graph Rewriting Semantics.” Mathematical Structures in Computer Science 6 (6): 579–612. https://doi.org/10.1017/S0960129500070109.
Bauer, Andrej. 2018a. Algebraic Effects and Handlers. https://github.com/OPLSS/introduction-to-algebraic-effects-and-handlers.
Bauer, Andrej. 2018b. “What Is Algebraic about Algebraic Effects and Handlers?” CoRR abs/1807.05923. https://arxiv.org/abs/1807.05923.
Bauer, Andrej. 2022. Dependent Types; Dependent Sums and Records. https://www.andrej.com/zapiski/ISRM-LOGRAC-2022/.
Bauer, Andrej, and Martín Hötzel Escardó. 2021. The Burali–Forti Paradox in Homotopy Type Theory and Univalent Foundations. https://math.andrej.com/2021/02/22/burali-forti-in-hott-uf/.
Bauer, Andrej, and Matija Pretnar. 2015. “Programming with Algebraic Effects and Handlers.” Journal of Logical and Algebraic Methods in Programming 84 (1): 108–23. https://doi.org/10.1016/j.jlamp.2014.02.001.
Bauer, Andrej, and Jaka Smrekar. 2019. Homotopy (Type) Theory. https://github.com/andrejbauer/homotopy-type-theory-course.
Baydin, Atilim Gunes, Barak A. Pearlmutter, Alexey Andreyevich Radul, and Jeffrey Mark Siskind. 2018. “Automatic Differentiation in Machine Learning: A Survey.” Journal of Machine Learning Research 18 (153): 1–43. https://jmlr.org/papers/v18/17-468.html.
Beluga Development Team. 2025. Beluga: A Framework for Programming and Reasoning with Deductive Systems. Source repository. https://github.com/Beluga-lang/Beluga.
Benke, Marcin, Peter Dybjer, and Patrik Jansson. 2003. “Universes for Generic Programs and Proofs in Dependent Type Theory.” Nordic Journal of Computing 10 (4): 265–89.
Benton, P. N. 1994. A Mixed Linear and Non-Linear Logic. UCAM-CL-TR-352. University of Cambridge Computer Laboratory. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-352.html.
Berg, Benno van den, and Richard Garner. 2011. “Types Are Weak Omega-Groupoids.” Proceedings of the London Mathematical Society 102 (2): 370–94. https://doi.org/10.1112/plms/pdq026.
Bernadet, Alexis, and Stéphane Graham-Lengrand. 2013. “Non-Idempotent Intersection Types and Strong Normalisation.” Logical Methods in Computer Science 9 (4:3): 1–44. https://doi.org/10.2168/LMCS-9(4:3)2013.
Bertot, Yves. 2006. CoInduction in Coq. https://arxiv.org/abs/cs/0603119.
Betarte, Gustavo, and Álvaro Tasistro. 1998. “Extension of Martin-Löf’s Type Theory with Record Types and Subtyping.” In Twenty-Five Years of Constructive Type Theory, edited by Giovanni Sambin and Jan M. Smith. Oxford University Press. https://doi.org/10.1093/oso/9780198501275.003.0004.
Beutner, Raven, C.-H. Luke Ong, and Fabian Zaiser. 2022. “Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming.” Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 536–51. https://doi.org/10.1145/3519939.3523721.
Bezem, Marc, Thierry Coquand, Peter Dybjer, and Martín Escardó. 2021. “On Generalized Algebraic Theories and Categories with Families.” Mathematical Structures in Computer Science 31 (9): 1006–23. https://doi.org/10.1017/S0960129521000268.
Bierhoff, Kevin. 2009. “API Protocol Compliance in Object-Oriented Software.” PhD Thesis CMU-ISR-09-108. Carnegie Mellon University. https://www.cs.cmu.edu/~kbierhof/thesis/bierhoff-thesis.pdf.
Bierhoff, Kevin, and Jonathan Aldrich. 2007. Modular Typestate Verification of Aliased Objects. CMU-ISRI-07-105. Carnegie Mellon University. https://www.cs.cmu.edu/~kbierhof/papers/typestate-tr.pdf.
Bierhoff, Kevin, Nels E. Beckman, and Jonathan Aldrich. 2009. “Practical API Protocol Checking with Access Permissions.” ECOOP 2009. https://doi.org/10.1007/978-3-642-03013-0_10.
Binder, David, Ingo Skupin, Tim Süberkrüb, and Klaus Ostermann. 2024. “Deriving Dependently-Typed OOP from First Principles.” Proceedings of the ACM on Programming Languages 8 (OOPSLA1). https://doi.org/10.1145/3649846.
Bird, Richard S., and Ross Paterson. 1999. “De Bruijn Notation as a Nested Datatype.” Journal of Functional Programming 9 (1): 77–91. https://doi.org/10.1017/S0956796899003366.
Birkedal, Lars, and Aleš Bizjak. 2023. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic.
Birkedal, Lars, Ranald Clouston, Bassel Mannaa, Rasmus Ejlers Møgelberg, Andrew M. Pitts, and Bas Spitters. 2020. “Modal Dependent Type Theory and Dependent Right Adjoints.” Mathematical Structures in Computer Science 30 (2): 118–38. https://doi.org/10.1017/S0960129519000197.
Bizjak, Aleš, and Rasmus Ejlers Møgelberg. 2020. “Denotational Semantics for Guarded Dependent Type Theory.” Mathematical Structures in Computer Science 30 (4). https://doi.org/10.1017/S0960129520000080.
Blackshear, Sam, John C. Mitchell, Todd Nowacki, and Shaz Qadeer. 2022. The Move Borrow Checker. https://arxiv.org/abs/2205.05181.
Blanqui, Frédéric. 2025. Lambda-Pi Calculus Modulo Rewriting: Theory and Application to Proof Systems Interoperability. https://blanqui.gitlabpages.inria.fr/teaching.html.
Bocquet, Rafaël. 2025. “Relative Induction Principles for Second-Order Generalized Algebraic Theories.” PhD thesis, Eötvös Loránd University. https://rafaelbocquet.gitlab.io/pdfs/thesis.pdf.
Boer, Frank S. de, and Marcello M. Bonsangue. 2021. “Symbolic Execution Formally Explained.” Formal Aspects of Computing 33: 617–36. https://doi.org/10.1007/s00165-020-00527-y.
Boer, Menno de. 2020. “A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory.” Master’s thesis, Stockholm University. https://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-183834.
Boruch-Gruszecki, Aleksander, Jonathan Immanuel Brachthäuser, Edward Lee, Ondrej Lhotak, and Martin Odersky. 2021. Tracking Captured Variables in Types. https://arxiv.org/abs/2105.11896.
Bosman, Roger, Birthe van den Berg, Wenhao Tang, and Tom Schrijvers. 2024. “A Calculus for Scoped Effects and Handlers.” Logical Methods in Computer Science 20 (4): 17:1–50. https://doi.org/10.46298/LMCS-20(4:17)2024.
Bove, Ana, and Venanzio Capretta. 2005. “Modelling General Recursion in Type Theory.” Mathematical Structures in Computer Science 15 (4): 671–708. https://doi.org/10.1017/S0960129505004822.
Bove, Ana, Alexander Krauss, and Matthieu Sozeau. 2016. “Partiality and Recursion in Interactive Theorem Provers—an Overview.” Mathematical Structures in Computer Science 26 (1): 38–88. https://doi.org/10.1017/S0960129514000115.
Bowman, William J., Youyou Cong, Nick Rioux, and Amal Ahmed. 2018. “Type-Preserving CPS Translation of Sigma and Pi Types Is Not Not Possible.” Proceedings of the ACM on Programming Languages 2 (POPL): 22:1–33. https://doi.org/10.1145/3158110.
Brachthäuser, Jonathan Immanuel, Philipp Schuster, Edward Lee, and Aleksander Boruch-Gruszecki. 2022. “Effects, Capabilities, and Boxes.” Proceedings of the ACM on Programming Languages 6 (OOPSLA1). https://doi.org/10.1145/3527320.
Brachthäuser, Jonathan Immanuel, Philipp Schuster, and Klaus Ostermann. 2020. Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism. https://doi.org/10.1145/3428194.
Brookes, Stephen. 2007. “A Semantics for Concurrent Separation Logic.” Theoretical Computer Science 375 (1–3): 227–70. https://doi.org/10.1016/j.tcs.2006.12.034.
Brown, Matt, and Jens Palsberg. 2016. “Breaking Through the Normalization Barrier: A Self-Interpreter for Fω.” Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA), 5–17. https://doi.org/10.1145/2837614.2837623.
Bruce, Kim B. 2002. F-Bounded Polymorphism and Matching. https://cs.pomona.edu/~Kim/cs334/s02/Lectures/Lec20/Lec20.html.
Bruce, Kim B., Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin C. Pierce. 1995. “On Binary Methods.” Theory and Practice of Object Systems 1 (3): 221–42. https://doi.org/10.1002/j.1096-9942.1995.tb00019.x.
Brunerie, Guillaume, Axel Ljungström, and Anders Mörtberg. 2022. “Synthetic Integral Cohomology in Cubical Agda.” CSL 2022, Leibniz international proceedings in informatics, vol. 216: 11:1–19. https://doi.org/10.4230/LIPIcs.CSL.2022.11.
Buchholtz, Ulrik, and Mark Williams. 2024. Synthetic Homotopy Theory with HoTT/UF. https://ulrikbuchholtz.dk/mgs2024-synthetic-homotopy-theory.pdf.
Cai, Yufei, Paolo G. Giarrusso, and Klaus Ostermann. 2016. “System Fω with Equirecursive Types for Datatype-Generic Programming.” Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 30–43. https://doi.org/10.1145/2837614.2837660.
Caires, Luís, Frank Pfenning, and Bernardo Toninho. 2011. Session Types as Intuitionistic Linear Propositions. CMU-CS-11-138. Carnegie Mellon University. https://www.cs.cmu.edu/~fp/papers/CMU-CS-11-138.pdf.
Canning, Peter, William Cook, Walter Hill, Walter Olthoff, and John C. Mitchell. 1989. “F-Bounded Polymorphism for Object-Oriented Programming.” Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, 273–80. https://doi.org/10.1145/99370.99392.
Capretta, Venanzio. 2005. “General Recursion via Coinductive Types.” Logical Methods in Computer Science 1 (2). https://doi.org/10.2168/LMCS-1(2:1)2005.
Cardelli, Luca, and Peter Wegner. 1985. “On Understanding Types, Data Abstraction, and Polymorphism.” ACM Computing Surveys 17 (4): 471–523. https://doi.org/10.1145/6041.6042.
Carette, Jacques, Oleg Kiselyov, and Chung-chieh Shan. 2009. “Finally Tagless, Partially Evaluated: Tagless Staged Interpreters for Simpler Typed Languages.” Journal of Functional Programming 19 (5): 509–43. https://doi.org/10.1017/S0956796809007205.
Cartmell, John. 1978. “Generalised Algebraic Theories and Contextual Categories.” PhD thesis, University of Oxford. https://ncatlab.org/nlab/files/Cartmell-Thesis.pdf.
Cartmell, John. 1986. “Generalised Algebraic Theories and Contextual Categories.” Annals of Pure and Applied Logic 32 (3): 209–43. https://doi.org/10.1016/0168-0072(86)90053-9.
Cartmell, John. 2014. Meta-Theory of Generalised Algebraic Theories. https://www.entitymodelling.org/downloads/MetaGAT_3Oct2014.pdf.
Cartmell, John. 2018. The Generalised Algebraic Theory of Contextual Categories. https://entitymodelling.org/downloads/theGATofCCs_10Jan2018.pdf.
Castagna, Giuseppe. 2024. Programming with Union, Intersection, and Negation Types. https://doi.org/10.48550/arXiv.2111.03354.
Castagna, Giuseppe, Mickaël Laurent, Kim Nguyen, and Matthew Lutze. 2022. “On Type-Cases, Union Elimination, and Occurrence Typing.” Proceedings of the ACM on Programming Languages 6 (POPL): 1–31. https://doi.org/10.1145/3498674.
Castañeda, Armando, Sergio Rajsbaum, and Michel Raynal. 2015. “Specifying Concurrent Problems: Beyond Linearizability and up to Tasks.” Distributed Computing, Lecture notes in computer science, vol. 9363: 420–35. https://doi.org/10.1007/978-3-662-48653-5_28.
Castellan, Simon, Pierre Clairambault, and Peter Dybjer. 2017. “Undecidability of Equality in the Free Locally Cartesian Closed Category.” Logical Methods in Computer Science 13 (4): 22:1–38. https://doi.org/10.23638/LMCS-13(4:22)2017.
Castellan, Simon, Pierre Clairambault, and Peter Dybjer. 2021. “Categories with Families: Unityped, Simply Typed, and Dependently Typed.” In Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, edited by Claudia Casadio and Philip J. Scott, vol. 20. Outstanding Contributions to Logic. Springer. https://doi.org/10.1007/978-3-030-66545-6_5.
Castéran, Pierre, and Matthieu Sozeau. 2016. A Gentle Introduction to Type Classes and Relations in Coq. https://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf.
Cavallo, Evan, and Thierry Coquand. 2026. “Type-Theoretic Replacement and Univalent Completion: Applications and Interpretations.” TYPES 2025, Leibniz international proceedings in informatics, vol. 384: 10:1–27. https://doi.org/10.4230/LIPIcs.TYPES.2025.10.
Cedille Development Team. 2025. Cedille Cast: Programming and Proving Tutorials. https://github.com/cedille/cedille-cast.
Chakravarty, Manuel M. T., Gabriele Keller, and Simon Peyton Jones. 2005. “Associated Type Synonyms.” Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, 241–53. https://doi.org/10.1145/1086365.1086397.
Champin, Camil, and Samuel Mimram. 2024. Delooping Generated Groups in Homotopy Type Theory: Agda Proofs. Released. https://doi.org/10.4230/artifacts.22463.
Champin, Camil, Samuel Mimram, and Émile Oleon. 2024. “Delooping Generated Groups in Homotopy Type Theory.” FSCD 2024, Leibniz international proceedings in informatics, vol. 299: 6:1–20. https://doi.org/10.4230/LIPIcs.FSCD.2024.6.
Champin, Camil, Samuel Mimram, and Émile Oleon. 2026. Delooping Presented Groups in Homotopy Type Theory. https://arxiv.org/abs/2405.03264.
Chan, Jonathan, and Stephanie Weirich. 2023. Stratified Type Theory. https://arxiv.org/abs/2309.12164.
Chan, Jonathan, and Stephanie Weirich. 2025. Bounded First-Class Universe Levels in Dependent Type Theory. https://arxiv.org/abs/2502.20485.
Chapman, James, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. 2010. “The Gentle Art of Levitation.” Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, 3–14. https://doi.org/10.1145/1863543.1863547.
Charguéraud, Arthur. 2012. “The Locally Nameless Representation.” Journal of Automated Reasoning 49 (3): 363–408. https://doi.org/10.1007/s10817-011-9225-2.
Charguéraud, Arthur. 2025. Separation Logic Foundations, Volume 6 of Software Foundations. Released. https://github.com/DeepSpec/sf.
Chau, Chun Yin, and Lionel Parreaux. 2026. “The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic Union, Intersection, Negation, and Equi-Recursive Types.” Proceedings of the ACM on Programming Languages. https://doi.org/10.1145/3776689.
Cheney, James. 2009. “A Simple Nominal Type Theory.” Electronic Notes in Theoretical Computer Science 228 (3): 37–52. https://doi.org/10.1016/j.entcs.2008.12.115.
Cheney, James. 2012. “A Dependent Nominal Type Theory.” Logical Methods in Computer Science 8 (1:8). https://doi.org/10.2168/LMCS-8(1:8)2012.
Chlipala, Adam. 2008. “Parametric Higher-Order Abstract Syntax for Mechanized Semantics.” Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, 143–56. https://doi.org/10.1145/1411204.1411226.
Chlipala, Adam, and Cornell CS 6115 Staff. 2024. Week 14: Proof by Reflection. Cornell CS 6115 lecture. https://www.cs.cornell.edu/courses/cs6115/2024fa/lectures/lec16_reflection.html.
Christensen, J. Daniel, Morgan Opie, Egbert Rijke, and Luis Scoccola. 2020. “Localization in Homotopy Type Theory.” Higher Structures 4 (1): 1–32. https://doi.org/10.21136/HS.2020.01.
Christiansen, David Thrane. 2018. Checking Dependent Types with Bidirectional Type Checking and Normalization by Evaluation. Tutorial notes and literate implementations. https://davidchristiansen.dk/tutorials/.
Church, Alonzo. 1936. “An Unsolvable Problem of Elementary Number Theory.” American Journal of Mathematics 58 (2): 345–63. https://doi.org/10.2307/2371045.
Clouston, Ranald. 2018. “Fitch-Style Modal Lambda Calculi.” Foundations of Software Science and Computation Structures, Lecture notes in computer science, vol. 10803: 258–75. https://doi.org/10.1007/978-3-319-89366-2_14.
Clutch and Eris Team. 2026. Clutch and Eris: Probabilistic Relational Reasoning and Error Credits. https://clutch-project.org/epit2026.html.
Coblenz, Michael. 2024. Gradual Typing. https://cseweb.ucsd.edu/~mcoblenz/teaching/291B00_fall2024/slides/13_gradual_typing.pdf.
Cockx, Jesper. 2017. “Dependent Pattern Matching and Proof-Relevant Unification.” PhD thesis, KU Leuven.
Cockx, Jesper. 2020. “Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules.” 25th International Conference on Types for Proofs and Programs (TYPES 2019), Leibniz international proceedings in informatics, vol. 175: 2:1–27. https://doi.org/10.4230/LIPIcs.TYPES.2019.2.
Cockx, Jesper. 2026. Coinduction in Agda. https://gitlab.tudelft.nl/jcockx/agda-coinduction.
Cockx, Jesper, and Andreas Abel. 2020. “Elaborating Dependent (Co)pattern Matching: No Pattern Left Behind.” Journal of Functional Programming 30: e2. https://doi.org/10.1017/S0956796819000182.
Cockx, Jesper, Dominique Devriese, and Frank Piessens. 2016. “Eliminating Dependent Pattern Matching Without K.” Journal of Functional Programming 26: e16. https://doi.org/10.1017/S0956796816000174.
Cohen, Cyril, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. “Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.” In 21st International Conference on Types for Proofs and Programs (TYPES 2015), edited by Tarmo Uustalu, vol. 69. Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
Cohen, Cyril, Enzo Crance, and Assia Mahboubi. 2024a. Trocq 0.1.5: ESOP 2024 Artifact. V. 0.1.5. Released. https://doi.org/10.5281/zenodo.10563382.
Cohen, Cyril, Enzo Crance, and Assia Mahboubi. 2024b. “Trocq: Proof Transfer for Free, with or Without Univalence.” Programming Languages and Systems, Lecture notes in computer science, vol. 14577: 239–68. https://doi.org/10.1007/978-3-031-57262-3_10.
Cohen, Cyril, Enzo Crance, and Assia Mahboubi. 2024c. “Trocq: Proof Transfer for Free, with or Without Univalence: Artifact.” Programming Languages and Systems, Lecture notes in computer science, vol. 14577: 269–70. https://doi.org/10.1007/978-3-031-57262-3_11.
Cohen, Cyril, Enzo Crance, Assia Mahboubi, and contributors. 2025. Trocq. V. 0.2.0. Released. https://doi.org/10.5281/zenodo.15746672.
Compagnoni, Adriana B., and David Aspinall. 1996. Subtyping Dependent Types. ECS-LFCS-96-347. Laboratory for Foundations of Computer Science, University of Edinburgh. https://www.lfcs.inf.ed.ac.uk/reports/96/ECS-LFCS-96-347/.
Constable, Robert L., Stuart F. Allen, H. M. Bromley, et al. 1986a. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall.
Constable, Robert L., Stuart F. Allen, H. M. Bromley, et al. 1986b. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall. https://nuprl-web.cs.cornell.edu/book/Contents.html.
Coquand, Thierry. 1986. An Analysis of Girard’s Paradox. RR-0531. INRIA.
Coquand, Thierry. 1994. “Infinite Objects in Type Theory.” Types for Proofs and Programs, Lecture notes in computer science, vol. 806: 62–78. https://doi.org/10.1007/3-540-58085-9_72.
Coquand, Thierry. 1996. “An Algorithm for Type-Checking Dependent Types.” Science of Computer Programming 26 (1–3): 167–77. https://doi.org/10.1016/0167-6423(95)00021-6.
Coquand, Thierry. 2013. “Presheaf Model of Type Theory.” https://www.cse.chalmers.se/~coquand/presheaf.pdf.
Coquand, Thierry. 2019. “Canonicity and Normalisation for Dependent Type Theory.” Theoretical Computer Science 777: 184–91. https://doi.org/10.1016/j.tcs.2019.01.015.
Coquand, Thierry. 2023. A Variation of Reynolds–Hurkens Paradox. https://arxiv.org/abs/2308.16726.
Coquand, Thierry, and Gérard Huet. 1988. “The Calculus of Constructions.” Information and Computation 76 (2–3): 95–120. https://doi.org/10.1016/0890-5401(88)90005-3.
Coquand, Thierry, and Christine Paulin-Mohring. 1990. “Inductively Defined Types.” COLOG-88, Lecture notes in computer science, vol. 417: 50–66. https://doi.org/10.1007/3-540-52335-9_47.
Coquand, Thierry, Randy Pollack, and Makoto Takeyama. 2003a. “A Logical Framework with Dependently Typed Records.” In Typed Lambda Calculi and Applications, edited by Martin Hofmann, vol. 2701. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/3-540-44904-3_8.
Coquand, Thierry, Randy Pollack, and Makoto Takeyama. 2003b. “A Logical Framework with Dependently Typed Records.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 2701: 105–19. https://doi.org/10.1007/3-540-44904-3_8.
Correnson, Arthur, and Dominic Steinhöfel. 2023. “Engineering a Formally Verified Automated Bug Finder.” Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 1165–76. https://doi.org/10.1145/3611643.3616290.
Cousot, Patrick. 1997. “Types as Abstract Interpretations.” Conference Record of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 316–31. https://doi.org/10.1145/263699.263744.
Cousot, Patrick. 2015. A Gentle Introduction to Abstract Interpretation. https://www.di.ens.fr/~cousot/COUSOTtalks/TASE-15-tutorial.shtml.
Cousot, Patrick. 2019. “Syntactic and Semantic Soundness of Structural Dataflow Analysis.” Static Analysis, Lecture notes in computer science, vol. 11822: 96–117. https://doi.org/10.1007/978-3-030-32304-2_6.
Cousot, Patrick, and Radhia Cousot. 1977. “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.” Conference Record of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 238–52. https://doi.org/10.1145/512950.512973.
Crary, Karl. 2021. “A Focused Solution to the Avoidance Problem.” Journal of Functional Programming 31. https://doi.org/10.1017/S0956796820000222.
Crichton, Will, Gavin Gray, and Shriram Krishnamurthi. 2023. “A Grounded Conceptual Model for Ownership Types in Rust.” Proceedings of the ACM on Programming Languages 7 (OOPSLA2). https://doi.org/10.1145/3622841.
Crichton, Will, Marco Patrignani, Maneesh Agrawala, and Pat Hanrahan. 2022. “Modular Information Flow Through Ownership.” Proceedings of the ACM on Programming Languages 6 (PLDI). https://doi.org/10.1145/3519939.3523445.
Curien, Pierre-Louis. 2007. “Definability and Full Abstraction.” Electronic Notes in Theoretical Computer Science 172: 301–10. https://doi.org/10.1016/j.entcs.2007.02.011.
Dagand, Pierre-Évariste, and Conor McBride. 2012. Elaborating Inductive Definitions. https://arxiv.org/abs/1210.6390.
Dagand, Pierre-Èvariste, and Conor McBride. 2014. “Transporting Functions Across Ornaments.” Journal of Functional Programming 24 (2–3): 316–83. https://doi.org/10.1017/S0956796814000069.
Dagand, Pierre-Évariste, Nicolas Tabareau, and Éric Tanter. 2018. “Foundations of Dependent Interoperability.” Journal of Functional Programming 28: e9. https://doi.org/10.1017/S0956796818000011.
Dal Lago, Ugo. 2022. “Implicit Computation Complexity in Higher-Order Programming Languages: A Survey in Memory of Martin Hofmann.” Mathematical Structures in Computer Science 32: 760–76. https://doi.org/10.1017/S0960129521000505.
Damas, Luis. 1985. “Type Assignment in Programming Languages.” PhD thesis, University of Edinburgh. https://era.ed.ac.uk/handle/1842/13555.
Damas, Luis, and Robin Milner. 1982. “Principal Type-Schemes for Functional Programs.” Proceedings of POPL 1982, 207–12. https://doi.org/10.1145/582153.582176.
Danielsson, Nils Anders. 2010. “Beating the Productivity Checker Using Embedded Languages.” Workshop on Partiality and Recursion in Interactive Theorem Provers, Electronic proceedings in theoretical computer science, vol. 43: 29–48. https://doi.org/10.4204/EPTCS.43.3.
Danielsson, Nils Anders, Naïm Camille Favier, and Ondřej Kubánek. 2026. “Normalisation for First-Class Universe Levels.” Proceedings of the ACM on Programming Languages 10 (POPL): 3:1–30. https://doi.org/10.1145/3776645.
Danos, Vincent, and Roberto Di Cosmo. 1997. The Linear Logic Primer. https://www.dicosmo.org/CourseNotes/LinLog/.
Danos, Vincent, and Laurent Regnier. 1989. “The Structure of Multiplicatives.” Archive for Mathematical Logic 28: 181–203. https://doi.org/10.1007/BF01622878.
Darais, David, and David Van Horn. 2019. “Constructive Galois Connections.” Journal of Functional Programming 29: e11. https://doi.org/10.1017/S0956796819000066.
Davies, Rowan, and Frank Pfenning. 2001. “A Modal Analysis of Staged Computation.” Journal of the ACM 48 (3): 555–604. https://doi.org/10.1145/382780.382785.
Deducteam. 2022. Dedukti. Version 2.7. https://github.com/Deducteam/Dedukti.
Deducteam. 2025. Lambdapi. V. 3.0.0. Released. https://github.com/Deducteam/lambdapi.
Diaconescu, Radu. 1975. “Axiom of Choice and Complementation.” Proceedings of the American Mathematical Society 51 (1): 176–78. https://doi.org/10.2307/2039868.
Docherty, Simon Robert. 2019. “Bunched Logics: A Uniform Approach.” PhD thesis, University College London. https://discovery.ucl.ac.uk/10073115/.
Dolan, Stephen. 2017. “Algebraic Subtyping.” PhD thesis, University of Cambridge.
Dolan, Stephen, and Alan Mycroft. 2017. “Polymorphism, Subtyping, and Type Inference in MLsub.” Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 60–72. https://doi.org/10.1145/3009837.3009882.
Dongol, Brijesh, and John Derrick. 2015. “Verifying Linearizability: A Comparative Survey.” ACM Computing Surveys 48 (2): 19:1–43. https://doi.org/10.1145/2796550.
Downen, Paul, and Zena M. Ariola. 2025. “A Contextual Formalization of Structural Coinduction.” Journal of Functional Programming, ahead of print. https://doi.org/10.1017/S0956796825100026.
Dreyer, Derek, Amal Ahmed, and Lars Birkedal. 2011. “Logical Step-Indexed Logical Relations.” Logical Methods in Computer Science 7 (2). https://doi.org/10.2168/LMCS-7(2:16)2011.
Dreyer, Derek, Robert Harper, Manuel M. T. Chakravarty, and Gabriele Keller. 2007. “Modular Type Classes.” Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 63–70. https://doi.org/10.1145/1190216.1190229.
Dreyer, Derek, Simon Spies, Lennard Gäher, et al. 2025. Semantics of Type Systems. https://plv.mpi-sws.org/semantics-course/.
Dudenhefner, Andrej. 2020. “Undecidability of Semi-Unification on a Napkin.” 5th International Conference on Formal Structures for Computation and Deduction, Leibniz international proceedings in informatics, vol. 167: 9:1–16. https://doi.org/10.4230/LIPIcs.FSCD.2020.9.
Dudenhefner, Andrej. 2023. “Constructive Many-One Reduction from the Halting Problem to Semi-Unification (Extended Version).” Logical Methods in Computer Science 19 (4): 22:1–27. https://doi.org/10.46298/lmcs-19(4:22)2023.
Dunfield, Jana, and Neelakantan R. Krishnaswami. 2019. Bidirectional Typing. https://doi.org/10.1145/3450952.
Dybjer, Peter. 1991. “Inductive Sets and Families in Martin-löf’s Type Theory and Their Set-Theoretic Semantics.” In Logical Frameworks. https://doi.org/10.1017/CBO9780511569807.012.
Dybjer, Peter. 1994. “Inductive Families.” Formal Aspects of Computing 6 (4): 440–65. https://doi.org/10.1007/BF01211308.
Dybjer, Peter. 1996. “Internal Type Theory.” In Types for Proofs and Programs, International Workshop TYPES ’95, Torino, Italy, June 5–8, 1995, Selected Papers, edited by Stefano Berardi and Mario Coppo, vol. 1158. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/3-540-61780-9_66.
Dybjer, Peter. 1997. “Representing Inductively Defined Sets by Wellorderings in Martin-löf’s Type Theory.” Theoretical Computer Science 176: 329–35. https://doi.org/10.1016/S0304-3975(96)00145-4.
Dybjer, Peter. 2000. “A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory.” The Journal of Symbolic Logic 65 (2): 525–49. https://doi.org/10.2307/2586554.
Dybjer, Peter, and Thierry Coquand. 1994. “Inductive Definitions and Type Theory: An Introduction.” Foundations of Software Technology and Theoretical Computer Science, Lecture notes in computer science, vol. 880. https://doi.org/10.1007/3-540-58715-2_114.
Edelman, Alan, and Steven G. Johnson. 2023. Matrix Calculus for Machine Learning and Beyond. https://ocw.mit.edu/courses/18-s096-matrix-calculus-for-machine-learning-and-beyond-january-iap-2023/.
Effekt contributors. 2026. Effekt Language Documentation and Compiler. https://effekt-lang.org/docs/concepts.
Ehrhard, Thomas, and Laurent Regnier. 2006. “Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms.” Computability in Europe 2006: Logical Approaches to Computational Barriers, Lecture notes in computer science, vol. 3988: 186–97. https://doi.org/10.1007/11780342_20.
Ehrhard, Thomas, and Laurent Regnier. 2008. “Uniformity and the Taylor Expansion of Ordinary Lambda-Terms.” Theoretical Computer Science 403 (2–3): 347–72. https://doi.org/10.1016/j.tcs.2008.06.001.
Eilenberg, Samuel, and Saunders Mac Lane. 1945. “General Theory of Natural Equivalences.” Transactions of the American Mathematical Society 58 (2): 231–94. https://doi.org/10.2307/1990284.
Eriksson, Oskar. 2025. Graded Modal Type Theory, Formalized. Licentiate thesis, University of Gothenburg and Chalmers University of Technology. https://research.chalmers.se/en/publication/546240.
Eriksson, Oskar, Andreas Abel, and Nils Anders Danielsson. 2026. “On Recursion in Graded Modal Type Theory.” Proceedings of the ACM on Programming Languages 10 (ICFP): 131–59. https://doi.org/10.1145/3828677.
Escardó, Martín. 2011. Running a Classical Proof with Choice in Agda. https://martinescardo.github.io/pigeon/.
Escardó, Martín Hötzel. 2023. Introduction to Univalent Foundations of Mathematics with Agda. https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/.
Escardó, Martín, and Paulo Oliva. 2014. Bar Recursion and Products of Selection Functions. https://arxiv.org/abs/1407.7046.
Escardó, Martín, Paulo Oliva, and Thomas Powell. 2011. “System t and the Product of Selection Functions.” Computer Science Logic, Leibniz international proceedings in informatics, vol. 12: 233–47. https://doi.org/10.4230/LIPIcs.CSL.2011.233.
Falco, Marc de. 2010. “An Explicit Framework for Interaction Nets.” Logical Methods in Computer Science 6 (4:6): 1–27. https://doi.org/10.2168/LMCS-6(4:6)2010.
(Favonia), Kuen-Bang Hou, Carlo Angiuli, and Reed Mullanix. 2023. “An Order-Theoretic Analysis of Universe Polymorphism.” Proceedings of the ACM on Programming Languages 7 (POPL): 1–27.
Fernández, Maribel, and Lionel Khalil. 2002. “Interaction Nets with McCarthy’s Amb.” Electronic Notes in Theoretical Computer Science 68 (2): 51–68. https://doi.org/10.1016/S1571-0661(05)80363-9.
Feser, Will. 2023. Gradual Typing. https://people.csail.mit.edu/feser/pld-s23/gradual_typing.html.
Findler, Robert Bruce, and Matthias Felleisen. 2002. “Contracts for Higher-Order Functions.” Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, 48–59. https://doi.org/10.1145/581478.581484.
Flanagan, Cormac. 2006. “Hybrid Type Checking.” Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 245–56. https://doi.org/10.1145/1111037.1111059.
Flatt, Matthew. 2016. “Binding as Sets of Scopes.” Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. https://doi.org/10.1145/2837614.2837620.
Fluet, Matthew, and Greg Morrisett. 2006. “Monadic Regions.” Journal of Functional Programming 16 (4–5). https://doi.org/10.1017/S0956796806006049.
Fluet, Matthew, Greg Morrisett, and Amal Ahmed. 2006. “Linear Regions Are All You Need.” Programming Languages and Systems, Lecture notes in computer science, vol. 3924: 7–21. https://doi.org/10.1007/11693024_2.
Forster, Yannick, Steven Schäfer, Simon Spies, and Kathrin Stark. 2019. “Call-by-Push-Value in Coq: Operational, Equational, and Denotational Theory.” Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 118–31. https://doi.org/10.1145/3293880.3294097.
Fourment, Joseph, and Yichen Xu. 2023. “A Mechanized Theory of the Box Calculus.” Proceedings of the 9th International Workshop on Aliasing, Confinement and Ownership. https://arxiv.org/abs/2309.05362.
Freeman, Tim, and Frank Pfenning. 1991. “Refinement Types for ML.” Proceedings of the 1991 ACM SIGPLAN Conference on Programming Language Design and Implementation, 268–77. https://doi.org/10.1145/113445.113468.
Friedman, Greg. 2012. “An Elementary Illustrated Introduction to Simplicial Sets.” Rocky Mountain Journal of Mathematics 42 (2): 353–423. https://doi.org/10.1216/RMJ-2012-42-2-353.
Frisch, Alain, Giuseppe Castagna, and Véronique Benzaken. 2008. “Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types.” Journal of the ACM 55 (4): 1–64. https://doi.org/10.1145/1391289.1391293.
Frumin, Dan. 2022. “Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq.” Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, 306–23. https://doi.org/10.1145/3497775.3503690.
Fu, Peng, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2020. “A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper.” CoRR abs/2005.08396. https://arxiv.org/abs/2005.08396.
Fu, Peng, Kohei Kishida, Neil J. Ross, and Peter Selinger. 2026. “Proto-Quipper with Reversing and Control.” Journal of Logical and Algebraic Methods in Programming 151: 101156. https://doi.org/10.1016/j.jlamp.2026.101156.
Fu, Peng, Kohei Kishida, and Peter Selinger. 2022. “Linear Dependent Type Theory for Quantum Programming Languages.” Logical Methods in Computer Science 18 (3): 28:1–44. https://doi.org/10.46298/LMCS-18(3:28)2022.
Fu, Peng, and Aaron Stump. 2014. “Self Types for Dependently Typed Lambda Encodings.” Joint Rewriting Techniques and Applications and Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 8560: 224–39. https://doi.org/10.1007/978-3-319-08918-8_16.
Gabbay, Murdoch J., and Andrew M. Pitts. 2002. “A New Approach to Abstract Syntax with Variable Binding.” Formal Aspects of Computing 13 (3–5): 341–63. https://doi.org/10.1007/s001650200016.
Gaboardi, Marco, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. “Combining Effects and Coeffects via Grading.” Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 476–89. https://doi.org/10.1145/2951913.2951939.
Garcia, Ronald, Eric Tanter, Roger Wolff, and Jonathan Aldrich. 2014. “Foundations of Typestate-Oriented Programming.” ACM Transactions on Programming Languages and Systems 36 (4). https://doi.org/10.1145/2629609.
Gaster, Benedict R., and Mark P. Jones. 1996. A Polymorphic Type System for Extensible Records and Variants. NOTTCS-TR-96-3. University of Nottingham. https://web.cecs.pdx.edu/~mpj/pubs/polyrec.html.
Gay, Simon J., Peter Thiemann, and Vasco T. Vasconcelos. 2020. “Duality of Session Types: The Final Cut.” Programming Language Approaches to Concurrency- and Communication-cEntric Software, Electronic proceedings in theoretical computer science, vol. 314: 23–33. https://doi.org/10.4204/EPTCS.314.3.
Gentzen, Gerhard. 1935. “Untersuchungen über Das Logische Schließen. I–II.” Mathematische Zeitschrift 39: 176–210, 405–31.
Geuvers, Herman. 2009. “Introduction to Type Theory.” In Language Engineering and Rigorous Software Development (LerNet ALFA Summer School 2008), vol. 5520. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/978-3-642-03153-3_1.
Ghelli, Giorgio. 1996. “Complexity of Kernel Fun Subtyping.” Proceedings of the First ACM SIGPLAN International Conference on Functional Programming, 134–45. https://doi.org/10.1145/232627.232629.
Gilbert, Gaëtan. 2017. “Formalising Real Numbers in Homotopy Type Theory.” Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). https://doi.org/10.1145/3018610.3018614.
Gilbert, Gaëtan, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. “Definitional Proof-Irrelevance Without K.” Proceedings of the ACM on Programming Languages 3 (POPL): 3:1–28. https://doi.org/10.1145/3290316.
Giménez, Eduardo. 1995. “Codifying Guarded Definitions with Recursive Schemes.” Types for Proofs and Programs, Lecture notes in computer science, vol. 996: 39–59. https://doi.org/10.1007/3-540-60579-7_3.
Giménez, Eduardo, and Pierre Castéran. 2007. A Tutorial on [Co-]inductive Types in Coq. LaBRI, Université Bordeaux. https://www.labri.fr/perso/casteran/RecTutorial.pdf.
Girard, Jean-Yves. 1972. “Interprétation Fonctionnelle Et élimination Des Coupures de l’arithmétique d’ordre Supérieur.” PhD thesis, Université Paris VII. https://girard.perso.math.cnrs.fr/These.pdf.
Girard, Jean-Yves. 1987. “Linear Logic.” Theoretical Computer Science 50: 1–101. https://doi.org/10.1016/0304-3975(87)90045-4.
Girard, Jean-Yves, Yves Lafont, and Paul Taylor. 1989. Proofs and Types. Cambridge Tracts in Theoretical Computer Science 7. Cambridge University Press.
Godefroid, Patrice, Nils Klarlund, and Koushik Sen. 2005. “DART: Directed Automated Random Testing.” Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 213–23. https://doi.org/10.1145/1065010.1065036.
Goerss, Paul G., and John F. Jardine. 2009. Simplicial Homotopy Theory. Modern Birkhäuser Classics. Birkhäuser. https://doi.org/10.1007/978-3-0346-0189-4.
Gonthier, Georges, Martı́n Abadi, and Jean-Jacques Lévy. 1992. “The Geometry of Optimal Lambda Reduction.” Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 15–26. https://doi.org/10.1145/143165.143172.
Gordon, Andrew D., and Cédric Fournet. 2009. Principles and Applications of Refinement Types. MSR-TR-2009-147. Microsoft Research. https://www.microsoft.com/en-us/research/publication/principles-and-applications-of-refinement-types/.
Gordon, Michael J. C. 1985. HOL: A Machine Oriented Formulation of Higher Order Logic. UCAM-CL-TR-68. University of Cambridge Computer Laboratory. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-68.html.
Gordon, Michael J. C. 2015. “Tactics for Proof.” Philosophical Transactions of the Royal Society A 373. https://doi.org/10.1098/rsta.2014.0234.
Graded Type Theory contributors. 2026. An Agda Formalization of a Graded Modal Type Theory with Erasure, First-Class Universe Levels and Opaque Definitions. Versions jfp-submission-2026-04-30. https://github.com/graded-type-theory/graded-type-theory.
Grathwohl, Hans Bugge. 2016. “Guarded Recursive Type Theory.” PhD thesis, Aarhus University. https://pure.au.dk/portal/en/publications/guarded-recursive-type-theory/.
Gratzer, Daniel. 2023. “Syntax and Semantics of Modal Type Theory.” PhD thesis, Aarhus University.
Graulund, Christian Uldal. 2021. “Type Theories for Reactive Programming.” PhD thesis, IT University of Copenhagen.
Green, Alexander S., Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. “An Introduction to Quantum Programming in Quipper.” Reversible Computation, Lecture notes in computer science, vol. 7948: 110–24. https://doi.org/10.1007/978-3-642-38986-3_10.
Griffin, Timothy G. 1990. “A Formulae-as-Types Notion of Control.” Proceedings of POPL, 47–58. https://doi.org/10.1145/96709.96714.
Grossman, Dan, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. 2001. Formal Type Soundness for Cyclone’s Region System. Nos. TR2001-1856. Cornell University.
Grossman, Dan, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. 2002. “Region-Based Memory Management in Cyclone.” Proceedings of PLDI 2002, 282–93. https://doi.org/10.1145/512529.512563.
Guerrini, Stefano. 1999. “Correctness of Multiplicative Proof Nets Is Linear.” Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, 454–63. https://doi.org/10.1109/LICS.1999.782640.
Gundry, Adam Michael. 2013. “Type Inference, Haskell and Dependent Types.” PhD thesis, University of Strathclyde. https://adam.gundry.co.uk/pub/thesis/thesis-2013-12-03.pdf.
Hall, Cordelia V., Kevin Hammond, Simon L. Peyton Jones, and Philip Wadler. 1996. “Type Classes in Haskell.” ACM Transactions on Programming Languages and Systems 18 (2): 109–38. https://doi.org/10.1145/227699.227700.
Harper, Robert. 2013. 15-819 Homotopy Type Theory. https://www.cs.cmu.edu/~rwh/courses/hott/.
Harper, Robert. 2016. Practical Foundations for Programming Languages. 2nd ed. Cambridge University Press. https://www.cs.cmu.edu/~rwh/pfpl.html.
Harper, Robert. 2021. Computational Type Theory. Carnegie Mellon University course notes. https://www.cs.cmu.edu/~rwh/courses/chtt/.
Harper, Robert. 2026. Dependent Type Theory: Programming and Proving. Advanced Topics in Programming Languages course handout. https://www.cs.cmu.edu/~rwh/courses/atpl/pdfs/dependency.pdf.
Harper, Robert, Bruce F. Duba, and David B. MacQueen. 1993. “Typing First-Class Continuations in ML.” Journal of Functional Programming 3 (4): 465–84. https://doi.org/10.1017/S095679680000085X.
Harper, Robert, Furio Honsell, and Gordon Plotkin. 1993. “A Framework for Defining Logics.” Journal of the ACM 40 (1): 143–84. https://doi.org/10.1145/138027.138060.
Harper, Robert, and Mark Lillibridge. 1993. A Type-Theoretic Approach to Higher-Order Modules with Sharing. CMU-CS-93-197 and CMU-CS-FOX-93-04. Carnegie Mellon University.
Harper, Robert, and Mark Lillibridge. 1994. “A Type-Theoretic Approach to Higher-Order Modules with Sharing.” Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 123–37. https://doi.org/10.1145/174675.176927.
Harper, Robert, and Robert Pollack. 1991. “Type Checking with Universes.” Theoretical Computer Science 89 (1): 107–36. https://doi.org/10.1016/0304-3975(90)90108-T.
Haselwarter, Philipp G., Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, and Lars Birkedal. 2024. “Tachis: Higher-Order Separation Logic with Credits for Expected Costs.” Proceedings of the ACM on Programming Languages 8 (OOPSLA2). https://doi.org/10.1145/3689753.
Hatcher, Allen. n.d. Notes on Introductory Point-Set Topology. https://pi.math.cornell.edu/~hatcher/Top/Topdownloads.html.
Hatti, Eashan, Arthur Oliveira Vale, Zhongye Wang, Yueyang Feng, and Zhong Shao. 2026. “A Complete Program Logic for Compositional Linearizability.” 40th European Conference on Object-Oriented Programming (ECOOP 2026), Leibniz international proceedings in informatics, vol. 372: 11:1–28. https://doi.org/10.4230/LIPIcs.ECOOP.2026.11.
Henglein, Fritz. 1993. “Type Inference with Polymorphic Recursion.” ACM Transactions on Programming Languages and Systems 15 (2): 253–89. https://doi.org/10.1145/169701.169692.
Henriksen, Troels, Niels G. W. Serup, Martin Elsman, Fritz Henglein, and Cosmin E. Oancea. 2017. “Futhark: Purely Functional GPU-Programming with Nested Parallelism and in-Place Array Updates.” Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 556–71. https://doi.org/10.1145/3062341.3062354.
Herbelin, Hugo. 2005. “On the Degeneracy of Σ-Types in Presence of Computational Classical Logic.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 3461: 209–20. https://doi.org/10.1007/11417170_16.
Herlihy, Maurice P., and Jeannette M. Wing. 1990. “Linearizability: A Correctness Condition for Concurrent Objects.” ACM Transactions on Programming Languages and Systems 12 (3): 463–92. https://doi.org/10.1145/78969.78972.
Heunen, Chris. 2026. Introduction to Quantum Programming and Semantics. https://opencourse.inf.ed.ac.uk/iqps.
Hickey, Jason. 1996. “Formal Objects in Type Theory Using Very Dependent Types.” Foundations of Object-Oriented Languages 3.
HigherOrderCO. 2026. HVM2. Released. https://github.com/HigherOrderCO/HVM2.
Hillerström, Daniel, Sam Lindley, and Robert Atkey. 2020. “Effect Handlers via Generalised Continuations.” Journal of Functional Programming 30: e5. https://doi.org/10.1017/S0956796820000040.
Hirsch, Andrew K., and Deepak Garg. 2021. Pirouette: Higher-Order Typed Functional Choreographies. MPI-SWS-2021-004. Max Planck Institute for Software Systems. https://arxiv.org/abs/2111.03484.
Hoffmann, Jan. 2024. G"odel’s System t and Properties of System t. https://www.cs.cmu.edu/~janh/courses/814/24/.
Hoffmann, Jan, and Martin Hofmann. 2010. “Amortized Resource Analysis with Polynomial Potential: A Static Inference of Polynomial Bounds for Functional Programs.” Programming Languages and Systems, Lecture notes in computer science, vol. 6012: 287–306. https://doi.org/10.1007/978-3-642-11957-6_16.
Hofmann, Martin. 1995. “Extensional Concepts in Intensional Type Theory.” PhD thesis, University of Edinburgh. https://era.ed.ac.uk/handle/1842/399.
Hofmann, Martin. 1997. “Syntax and Semantics of Dependent Types.” In Semantics and Logics of Computation, edited by Andrew M. Pitts and Peter Dybjer, vol. 14. Publications of the Newton Institute. Cambridge University Press. https://doi.org/10.1017/CBO9780511526619.004.
Hofmann, Martin, and Thomas Streicher. 1994. “The Groupoid Model Refutes Uniqueness of Identity Proofs.” Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, 208–12. https://doi.org/10.1109/LICS.1994.316071.
Hofmann, Martin, and Thomas Streicher. 1998. “The Groupoid Interpretation of Type Theory.” In Twenty-Five Years of Constructive Type Theory, edited by Giovanni Sambin and Jan M. Smith, vol. 36. Oxford Logic Guides. Oxford University Press. https://doi.org/10.1093/oso/9780198501275.003.0008.
HOL4 developers. 2026. HOL4 Official Documentation. https://hol-theorem-prover.org/docs/trindemossen-2/.
Holtzen, Steven. 2024. Probabilistic Programming Languages. https://www.khoury.northeastern.edu/home/sholtzen/oplss24-ppl/.
Honda, Kohei, Nobuko Yoshida, and Marco Carbone. 2016. “Multiparty Asynchronous Session Types.” Journal of the ACM 63 (1): 9:1–67. https://doi.org/10.1145/2827695.
Hou (Favonia), Kuen-Bang, and Robert Harper. 2018. “Covering Spaces in Homotopy Type Theory.” TYPES 2016, Leibniz international proceedings in informatics, vol. 97: 11:1–16. https://doi.org/10.4230/LIPIcs.TYPES.2016.11.
Hou (Favonia), Kuen-Bang, and Michael Shulman. 2016. “The Seifert–van Kampen Theorem in Homotopy Type Theory.” CSL 2016, Leibniz international proceedings in informatics, vol. 62: 22:1–16. https://doi.org/10.4230/LIPIcs.CSL.2016.22.
Hsu, Justin. 2021. Reasoning about Probabilistic Programs. https://justinhsu.net/files/slides/oplss21.pdf.
Hu, Jason Z. S., and Ondřej Lhoták. 2020. “Undecidability of D<: And Its Decidable Fragments.” Proceedings of the ACM on Programming Languages 4 (POPL): 9:1–30. https://doi.org/10.1145/3371077.
Huang, Xu. 2023. Synthetic Tait Computability the Hard Way. https://arxiv.org/abs/2310.02051.
Hubers, Alex, and J. Garrett Morris. 2023a. “Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc.” Proceedings of the ACM on Programming Languages 7 (ICFP). https://doi.org/10.1145/3607843.
Hubers, Alex, and J. Garrett Morris. 2023b. “Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc.” Proceedings of the ACM on Programming Languages 7 (ICFP): 1–29. https://doi.org/10.1145/3607843.
Hurewicz, Witold. 1955. “On the Concept of Fiber Space.” Proceedings of the National Academy of Sciences 41 (11): 956–61. https://doi.org/10.1073/pnas.41.11.956.
Hurkens, Antonius J. C. 1995. “A Simplification of Girard’s Paradox.” In Typed Lambda Calculi and Applications, edited by Mariangiola Dezani-Ciancaglini and Gordon Plotkin, vol. 902. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/BFb0014058.
Hyland, J. M. E. 1982. “The Effective Topos.” In The l. E. J. Brouwer Centenary Symposium, edited by A. S. Troelstra and D. van Dalen, vol. 110. Studies in Logic and the Foundations of Mathematics. North-Holland. https://doi.org/10.1016/S0049-237X(09)70129-6.
Idris 2 Contributors. 2026. Multiplicities in Idris 2. https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html.
Jacobs, Bart. 1999. Categorical Logic and Type Theory. Vol. 141. Studies in Logic and the Foundations of Mathematics. North-Holland / Elsevier.
Jacobs, Bart, and Tom Melham. 1993. “Translating Dependent Type Theory into Higher Order Logic.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 664: 209–29. https://doi.org/10.1007/BFb0037108.
Jansen, Nils, and Benjamin Lucien Kaminski. 2017. Probabilistic Programming. https://moves.rwth-aachen.de/teaching/ws-1617/probabilistic-programming/.
Jardine, J. F. 2018. Lectures on Homotopy Theory. https://www.math.uwo.ca/faculty/jardine/courses/homth/homotopy_theory.html.
Jeffrey, Alan. 2012. “LTL Types FRP: Linear-Time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs.” Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification, 49–60. https://doi.org/10.1145/2103776.2103783.
Jenkins, Christopher, Andrew Marmaduke, and Aaron Stump. 2022. “Simulating Large Eliminations in Cedille.” 27th International Conference on Types for Proofs and Programs, Leibniz international proceedings in informatics, vol. 239: 9:1–22. https://doi.org/10.4230/LIPIcs.TYPES.2021.9.
Jenkins, Christopher, and Aaron Stump. 2021. “Monotone Recursive Types and Recursive Data Representations in Cedille.” Mathematical Structures in Computer Science 31 (6): 682–745. https://doi.org/10.1017/S0960129521000402.
Jhala, Ranjit, Eric L. Seidel, and Niki Vazou. 2024. Programming with Refinement Types: An Introduction to LiquidHaskell. https://ucsd-progsys.github.io/liquidhaskell-tutorial/.
Jhala, Ranjit, and Niki Vazou. 2021. “Refinement Types: A Tutorial.” Foundations and Trends in Programming Languages 6 (3–4): 159–317. https://doi.org/10.1561/2500000032.
Jones, Mark P. 1992. Qualified Types: Theory and Practice. PRG-106. Oxford University Computing Laboratory. https://www.cs.ox.ac.uk/files/3432/PRG106.pdf.
Jones, Mark P. 1999. Typing Haskell in Haskell. https://web.cecs.pdx.edu/~mpj/thih/thih.pdf.
Jones, Neil D., Carsten K. Gomard, and Peter Sestoft. 1993. Partial Evaluation and Automatic Program Generation. Prentice Hall.
Jong, Tom de. 2025. Categorical Realizability. https://github.com/tomdjong/MGS-categorical-realizability.
Jonsson, Peter A., and Johan Nordlander. 2010. “Positive Supercompilation for a Higher-Order Call-by-Value Language.” Logical Methods in Computer Science 6 (3:5): 1–39. https://doi.org/10.2168/LMCS-6(3:5)2010.
Jónsson, Peter A. 2008. “Positive Supercompilation for a Higher-Order Call-by-Value Language.” PhD thesis, Luleå University of Technology.
Jónsson, Peter A. 2011. “Time- and Size-Efficient Supercompilation.” PhD thesis, Luleå University of Technology.
Jónsson, Peter A., and Johan Nordlander. 2008. Positive Supercompilation for a Higher-Order Call-by-Value Language: Extended Proofs. Luleå University of Technology.
Jourdan, Jacques-Henri, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. “A Formally-Verified C Static Analyzer.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 247–59. https://doi.org/10.1145/2676726.2676966.
Jung, Ralf. 2020. “Understanding and Evolving the Rust Programming Language.” PhD thesis, Saarland University. https://doi.org/10.22028/D291-31946.
Jung, Ralf, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018. “Iris from the Ground up: A Modular Foundation for Higher-Order Concurrent Separation Logic.” Journal of Functional Programming 28: e20. https://doi.org/10.1017/S0956796818000151.
Jung, Ralf, David Swasey, Filip Sieczkowski, et al. 2015. “Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.” Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 637–50. https://doi.org/10.1145/2676726.2676980.
Junttila, Tommi. 2020. A Theory Solver for Difference Logic. https://users.aalto.fi/~tjunttil/2020-DP-AUT/notes-smt/diff_solver.html.
Kameyama, Yukiyoshi, and Masahito Hasegawa. 2003. “A Sound and Complete Axiomatization of Delimited Continuations.” Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), 177–88. https://doi.org/10.1145/944705.944722.
Kammar, Ohad. 2026. Foundations for Type-Driven Probabilistic Modelling. https://denotational.co.uk/tdpm-aarhus-course-2026/.
Kaposi, Ambrus, András Kovács, and Ambroise Lafont. 2020. “For Finitary Induction-Induction, Induction Is Enough.” 25th International Conference on Types for Proofs and Programs (TYPES 2019), Leibniz international proceedings in informatics, vol. 175: 6:1–30. https://doi.org/10.4230/LIPIcs.TYPES.2019.6.
Kapulkin, Chris, and Peter LeFanu Lumsdaine. 2020. “The Law of Excluded Middle in the Simplicial Model of Type Theory.” Theory and Applications of Categories 35 (40): 1546–48. https://arxiv.org/abs/2006.13694.
Kapulkin, Chris, and Peter LeFanu Lumsdaine. 2021. “The Simplicial Model of Univalent Foundations (After Voevodsky).” Journal of the European Mathematical Society 23 (6): 2071–126. https://doi.org/10.4171/JEMS/1050.
Kapulkin, Krzysztof, and Yufeng Li. 2025. “Extensional Concepts in Intensional Type Theory, Revisited.” Theoretical Computer Science 1029: 115051. https://doi.org/10.1016/j.tcs.2024.115051.
Kawata, Akira, and Atsushi Igarashi. 2019a. A Dependently Typed Multi-Stage Calculus. https://arxiv.org/abs/1908.02035.
Kawata, Akira, and Atsushi Igarashi. 2019b. “A Dependently Typed Multi-Stage Calculus.” Programming Languages and Systems—APLAS 2019, Lecture notes in computer science, vol. 11893: 53–72. https://doi.org/10.1007/978-3-030-34175-6_4.
Kennedy, Andrew John. 1996. “Programming Languages and Dimensions.” PhD Thesis UCAM-CL-TR-391. University of Cambridge. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf.
Kfoury, A. J., and Jerzy Tiuryn. 1992. “Type Reconstruction in Finite-Rank Fragments of the Second-Order Lambda-Calculus.” Information and Computation 98 (2): 228–57. https://doi.org/10.1016/0890-5401(92)90020-G.
King, James C. 1976. “Symbolic Execution and Program Testing.” Communications of the ACM 19 (7): 385–94. https://doi.org/10.1145/360248.360252.
Kohlenbach, Ulrich. 1998. Proof Interpretations. LS-98-1. BRICS Lecture Series. BRICS, University of Aarhus. https://www.brics.dk/LS/98/1/BRICS-LS-98-1.pdf.
Kopylov, Alexei. 2003. “Dependent Intersection: A New Way of Defining Records in Type Theory.” 18th Annual IEEE Symposium on Logic in Computer Science, 86–95. https://doi.org/10.1109/LICS.2003.1210048.
Kovács, András. 2020. “Elaboration with First-Class Implicit Function Types.” Proceedings of the ACM on Programming Languages 4 (ICFP): 1–29. https://doi.org/10.1145/3408983.
Kovács, András. 2022. Generalized Universe Hierarchies and First-Class Universe Levels. https://arxiv.org/abs/2103.00223.
Kovács, András. 2026a. “Canonicity for Indexed Inductive-Recursive Types.” Proceedings of the ACM on Programming Languages 10 (POPL). https://doi.org/10.1145/3776685.
Kovács, András. 2026b. Elaboration Zoo: Minimal Implementations for Dependent Type Checking and Elaboration. Git repository. https://github.com/AndrasKovacs/elaboration-zoo.
Kovács, András. 2026c. Smalltt: High-Performance Elaboration with Dependent Types. Software and design notes. https://github.com/AndrasKovacs/smalltt.
Kraus, Nicolai, Fredrik Nordvall Forsberg, and Chuangjie Xu. 2023. “Type-Theoretic Approaches to Ordinals.” Theoretical Computer Science 957: 113843. https://doi.org/10.1016/j.tcs.2023.113843.
Krauss, Alexander. 2026. Defining Recursive Functions in Isabelle/HOL. https://isabelle.in.tum.de/doc/functions.pdf.
Kreitz, Christoph. 2002. The Nuprl Proof Development System, Version 5: Reference Manual and User’s Guide. Cornell University. https://www.cs.cornell.edu/info/people/kreitz/PDF/02cucs-NuprlManual.pdf.
Krishnamurthi, Shriram. 2014. Objects: Interpretation and Types. https://papl.cs.brown.edu/2014/objects.html.
Kruskal, Joseph B. 1960. “Well-Quasi-Ordering, the Tree Theorem, and vázsonyi’s Conjecture.” Transactions of the American Mathematical Society 95 (2): 210–25. https://doi.org/10.1090/S0002-9947-1960-0111704-1.
Kudasov, Nikolai, Violetta Sim, and Benedikt Ahrens. 2026. Rzk: A Proof Assistant for Synthetic Infinity-Categories. https://arxiv.org/abs/2607.12207.
Kumar, Ramana, Rob Arthan, Magnus O. Myreen, and Scott Owens. 2014. “HOL with Definitions: Semantics, Soundness, and a Verified Implementation.” Interactive Theorem Proving, Lecture notes in computer science, vol. 8558: 308–24. https://doi.org/10.1007/978-3-319-08970-6_20.
Lafont, Yves. 1990. “Interaction Nets.” Proceedings of POPL 1990, 95–108. https://doi.org/10.1145/96709.96718.
Lafont, Yves. 1997. “Interaction Combinators.” Information and Computation 137 (1): 69–101. https://doi.org/10.1006/inco.1997.2643.
Lafont, Yves. 2004. “Soft Linear Logic and Polynomial Time.” Theoretical Computer Science 318 (1–2): 163–80. https://doi.org/10.1016/j.tcs.2003.10.018.
Laird, James. 2023. “Revisiting Decidable Bounded Quantification, via Dinaturality.” Electronic Notes in Theoretical Informatics and Computer Science 1. https://doi.org/10.46298/entics.10474.
Lambek, Joachim. 1958. “The Mathematics of Sentence Structure.” The American Mathematical Monthly 65 (3): 154–70. https://doi.org/10.2307/2310058.
Laurent, Olivier. 2013. An Introduction to Proof Nets. https://www.irif.fr/~faggian/LMFI_2025/pn_notes.pdf.
Laurent, Théo, Meven Lennon-Bertrand, and Kenji Maillard. 2023. Definitional Functoriality for Dependent (Sub)types. https://arxiv.org/abs/2310.14929.
Laurent, Théo, Meven Lennon-Bertrand, and Kenji Maillard. 2024. “Definitional Functoriality for Dependent (Sub)types.” Programming Languages and Systems—ESOP 2024, Lecture notes in computer science, vol. 14576: 302–31. https://doi.org/10.1007/978-3-031-57262-3_13.
Lean Development Team. 2026. Lean Language Reference: Inductive Types and Recursive Definitions. https://lean-lang.org/doc/reference/latest/.
Lean Team. 2026. Definitional Equality. Lean Reference Manual: The Type System. https://lean-lang.org/doc/reference/latest/The-Type-System/.
Lee, Chin Soon, Neil D. Jones, and Amir M. Ben-Amram. 2001. “The Size-Change Principle for Program Termination.” Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 81–92. https://doi.org/10.1145/360204.360210.
Leijen, Daan. 2004. First-Class Labels for Extensible Rows. UU-CS-2004-051. Utrecht University.
Leijen, Daan. 2005. “Extensible Records with Scoped Labels.” Proceedings of the 2005 Symposium on Trends in Functional Programming, 297–312.
Leijen, Daan. 2014. “Koka: Programming with Row-Polymorphic Effect Types.” In Proceedings of the 5th Workshop on Mathematically Structured Functional Programming, edited by Neelakantan R. Krishnaswami and Paul Blain Levy, vol. 153. Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/EPTCS.153.8.
Lennon-Bertrand, Meven. 2022. “Bidirectional Typing for the Calculus of Inductive Constructions.” PhD thesis, Nantes Université. https://www.meven.ac/documents/22-phd.pdf.
Lennon-Bertrand, Meven, Kenji Maillard, Nicolas Tabareau, and Éric Tanter. 2022. “Gradualizing the Calculus of Inductive Constructions.” ACM Transactions on Programming Languages and Systems 44 (2): 1–82. https://doi.org/10.1145/3495528.
Lennon-Bertrand, Meven, Andrew M. Pitts, Glynn Winskel, and Marcelo Fiore. 2024. Lecture Notes on Denotational Semantics. https://www.cl.cam.ac.uk/teaching/2526/DenotSem/materials.html.
Leroy, Xavier. 1994. “Manifest Types, Modules, and Separate Compilation.” Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 109–22. https://doi.org/10.1145/174675.176926.
Leroy, Xavier. 2000. “A Modular Module System.” Journal of Functional Programming 10 (3): 269–303. https://doi.org/10.1017/S0956796800003683.
Leroy, Xavier. 2019. Happy Sisyphus: Infinite Types, Coinductive Proofs, and Reactive Programming. Collège de France lecture. https://www.college-de-france.fr/en/agenda/lecture/program-demonstrate-curry-howard-correspondence-today/happy-sisyphus-infinite-types-coinduction-demonstrations-and-reactive-programming.
Leroy, Xavier. 2026. Control Structures in Programming Languages: From Goto to Algebraic Effects. https://xavierleroy.org/control-structures/.
Leuschel, Michael. 2002. “Homeomorphic Embedding for Online Termination of Symbolic Methods.” The Essence of Computation: Complexity, Analysis, Transformation, Lecture notes in computer science, vol. 2566: 379–403. https://doi.org/10.1007/3-540-36377-7_17.
Levy, Paul Blain. 2001. “Call-by-Push-Value.” PhD thesis, Queen Mary; Westfield College, University of London. https://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf.
Levy, Paul Blain. 2026. Lambda-Calculus, Effects and Call-by-Push-Value. https://pblevy.github.io/mgs/effcbpv.html.
Li, John M., Amal Ahmed, and Steven Holtzen. 2023. “Lilac: A Modal Separation Logic for Conditional Probability.” Proceedings of the ACM on Programming Languages 7 (PLDI): 148–71. https://doi.org/10.1145/3591226.
Li, Peng, and Danfeng Zhang. 2017. Towards a Flow- and Path-Sensitive Information Flow Analysis. https://arxiv.org/abs/1706.01407.
Li, Yao, and Robert Harper. 2026. “Synthetic Tait Computability in Istari.” Proceedings of the 53rd ACM SIGPLAN Symposium on Principles of Programming Languages. https://doi.org/10.1145/3779031.3779085.
Licata, Daniel R., and Michael Shulman. 2013. Calculating the Fundamental Group of the Circle in Homotopy Type Theory. https://arxiv.org/abs/1301.3443.
Liepelt, Vilem, Danielle Marshall, and Dominic Orchard. 2026. “Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types.” Proceedings of the 2026 ACM SIGPLAN International Conference on Functional Programming. https://doi.org/10.1145/3828697.
Lieverse, Kayleigh Zoë. 2024. “A Generic Translation from Case Trees to Eliminators.” Master’s thesis, Delft University of Technology. https://repository.tudelft.nl/record/uuid:e91ef1ea-942e-4f11-a1c4-bb82f444aaed.
Lincoln, Patrick, John Mitchell, Andre Scedrov, and Natarajan Shankar. 1992. “Decision Problems for Propositional Linear Logic.” Annals of Pure and Applied Logic 56 (1–3): 239–311. https://doi.org/10.1016/0168-0072(92)90075-B.
Lindley, Sam. 2014. Algebraic Effects and Effect Handlers for Idioms and Arrows. https://doi.org/10.1145/2633628.2633636.
Loregian, Fosco. 2023. Coend Calculus. arXiv:1501.02503. https://arxiv.org/abs/1501.02503.
Lumsdaine, Peter LeFanu. 2010. “Weak Omega-Categories from Intensional Type Theory.” Logical Methods in Computer Science 6 (3:24): 1–19. https://doi.org/10.2168/LMCS-6(3:24)2010.
Lumsdaine, Peter LeFanu, and Michael Shulman. 2020. “Semantics of Higher Inductive Types.” Mathematical Proceedings of the Cambridge Philosophical Society 169: 159–208. https://doi.org/10.1017/S030500411900015X.
Luo, Zhaohui. 1994. Computation and Reasoning: A Type Theory for Computer Science. Vol. 11. International Series of Monographs on Computer Science. Oxford University Press. https://doi.org/10.1093/oso/9780198538356.001.0001.
Luo, Zhaohui. 1999. “Coercive Subtyping.” Journal of Logic and Computation 9 (2): 105–30. https://doi.org/10.1093/logcom/9.2.105.
Lurie, Jacob. 2026. Kerodon. https://kerodon.net/.
Lutze, Matthew, Magnus Madsen, Philipp Schuster, and Jonathan Immanuel Brachthäuser. 2023. “With or Without You: Programming with Effect Exclusion.” Proceedings of the ACM on Programming Languages 7 (ICFP): 204:1–28. https://doi.org/10.1145/3607846.
Ma, Cong, Zhaoyi Ge, Max Jung, and Yizhou Zhang. 2025. “Zero-Overhead Lexical Effect Handlers.” Proceedings of the ACM on Programming Languages 9 (OOPSLA2). https://doi.org/10.1145/3763177.
Ma, Cong, Zhaoyi Ge, Edward Lee, and Yizhou Zhang. 2024. “Lexical Effect Handlers, Directly.” Proceedings of the ACM on Programming Languages 8 (OOPSLA2): 2874–904. https://doi.org/10.1145/3689770.
Mac Lane, Saunders. 1998. Categories for the Working Mathematician. 2nd ed. Vol. 5. Graduate Texts in Mathematics. Springer. https://doi.org/10.1007/978-1-4757-4721-8.
Manzyuk, Oleksandr, Barak A. Pearlmutter, Alexey Andreyevich Radul, David R. Rush, and Jeffrey Mark Siskind. 2019. “Perturbation Confusion in Forward Automatic Differentiation of Higher-Order Functions.” Journal of Functional Programming 29: e12. https://doi.org/10.1017/S095679681900008X.
Maraist, John, Martin Odersky, David N. Turner, and Philip Wadler. 1999. “Call-by-Name, Call-by-Value, Call-by-Need and the Linear Lambda Calculus.” Theoretical Computer Science 228 (1–2): 175–210. https://doi.org/10.1016/S0304-3975(98)00358-2.
Maraist, John, Martin Odersky, and Philip Wadler. 1998. “The Call-by-Need Lambda Calculus.” Journal of Functional Programming 8 (3): 275–317. https://doi.org/10.1017/S0956796898003037.
Maranget, Luc. 2007. “Warnings for Pattern Matching.” Journal of Functional Programming 17 (3): 387–421. https://doi.org/10.1017/S0956796807006223.
Maranget, Luc. 2008. “Compiling Pattern Matching to Good Decision Trees.” Proceedings of the ACM SIGPLAN Workshop on ML, 35–46. https://doi.org/10.1145/1411304.1411311.
Marquet-Wagner, Julien. 2025. Solving Domain Equations Using l"ob Induction. https://cs.au.dk/~birke/papers/recdomloeb-tutorial.pdf.
Marshall, Danielle, and Dominic Orchard. 2024. “Functional Ownership Through Fractional Uniqueness.” Proceedings of the ACM on Programming Languages 8 (OOPSLA1): 131:1–31. https://doi.org/10.1145/3649848.
Marshall, Danielle, and Dominic A. Orchard. 2024. “Non-Linear Communication via Graded Modal Session Types.” Information and Computation 301: 105234. https://doi.org/10.1016/j.ic.2024.105234.
Martin-Löf, Per. 1975. “An Intuitionistic Theory of Types: Predicative Part.” In Logic Colloquium ’73, Proceedings of the Logic Colloquium, edited by H. E. Rose and J. C. Shepherdson, vol. 80. Studies in Logic and the Foundations of Mathematics. North-Holland.
Martin-Löf, Per. 1982. “Constructive Mathematics and Computer Programming.” In Logic, Methodology and Philosophy of Science VI, Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science, Hannover 1979, edited by L. Jonathan Cohen, Jerzy Łoś, Helmut Pfeiffer, and Klaus-Peter Podewski, vol. 104. Studies in Logic and the Foundations of Mathematics. North-Holland. https://doi.org/10.1016/S0049-237X(09)70189-2.
Martin-Löf, Per. 1984. Intuitionistic Type Theory: Notes by Giovanni Sambin. Vol. 1. Studies in Proof Theory. Bibliopolis.
Martin-Löf, Per. 1992. “Substitution Calculus.” Unpublished manuscript.
Martin-Löf, Per. 1996. “On the Meanings of the Logical Constants and the Justifications of the Logical Laws.” Nordic Journal of Philosophical Logic 1 (1): 11–60.
Martin-Löf, Per. 1998. “An Intuitionistic Theory of Types.” In Twenty-Five Years of Constructive Type Theory (Venice, 1995), edited by Giovanni Sambin and Jan M. Smith, vol. 36. Oxford Logic Guides. Oxford University Press.
Matsushita, Yusuke, and Hiromi Ishii. 2026. “Pure Borrow: Linear Haskell Meets Rust-Style Borrowing.” Proceedings of the ACM on Programming Languages 10 (PLDI): 303–27. https://doi.org/10.1145/3808259.
May, J. Peter. 1999. A Concise Course in Algebraic Topology. University of Chicago Press. https://www.math.uchicago.edu/~may/CONCISE/ConciseRevised.pdf.
McBride, Conor. 1999. “Dependently Typed Functional Programs and Their Proofs.” PhD thesis, University of Edinburgh. http://hdl.handle.net/1842/374.
McBride, Conor. 2001. The Derivative of a Regular Type Is Its Type of One-Hole Contexts. http://www.strictlypositive.org/diff.pdf.
McBride, Conor. 2014. EWSCS 2014 Generic Programming Course. https://github.com/pigworker/EWSCS14.
McBride, Conor. 2015. Datatypes of Datatypes. https://github.com/pigworker/SSGEP-DataData.
McBride, Conor. 2016. “I Got Plenty o’ Nuttin’.” A List of Successes That Can Change the World, Lecture notes in computer science, vol. 9600: 207–33. https://doi.org/10.1007/978-3-319-30936-1_12.
Melliès, Paul-André. 1995. “Typed Lambda-Calculi with Explicit Substitutions May Not Terminate.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 902: 328–34. https://doi.org/10.1007/BFb0014062.
Melliès, Paul-André. 2009. “Categorical Semantics of Linear Logic.” In Interactive Models of Computation and Program Behaviour, vol. 27. Panoramas Et Synthèses. Société Mathématique de France.
Mendler, Nax Paul. 1991. “Inductive Types and Type Constraints in the Second-Order Lambda Calculus.” Annals of Pure and Applied Logic 51 (1–2): 159–72. https://doi.org/10.1016/0168-0072(91)90069-X.
Milewski, Bartosz. 2026. Actegories, Tambara Equipment, and Profunctor Optics. https://bartoszmilewski.com/2026/07/19/profunctor-optics/.
Miller, Haynes. 2020. Algebraic Topology II. https://ocw.mit.edu/courses/18-906-algebraic-topology-ii-spring-2020/.
Milner, Robin. 1979. “LCF: A Way of Doing Proofs with a Machine.” Mathematical Foundations of Computer Science 1979. https://doi.org/10.1007/3-540-09526-8_11.
Mimram, Samuel. 2020. Program = Proof. https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/pp/course.pdf.
Miné, Antoine. 2017. “Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation.” Foundations and Trends in Programming Languages 4 (3–4): 120–372. https://doi.org/10.1561/2500000034.
Miquey, Étienne. 2017. “Classical Realizability and Side-Effects.” PhD thesis, Université Paris-Diderot; Universidad de la República. https://www.i2m.univ-amu.fr/perso/etienne.miquey/these/.
Miquey, Étienne. 2019. “A Classical Sequent Calculus with Dependent Types.” ACM Transactions on Programming Languages and Systems 41 (2): 1–47. https://doi.org/10.1145/3230625.
Mitchell, John C., and Gordon D. Plotkin. 1988. “Abstract Types Have Existential Type.” ACM Transactions on Programming Languages and Systems 10 (3): 470–502. https://doi.org/10.1145/44501.45065.
Møgelberg, Rasmus Ejlers, and Alex Simpson. 2009. “Relational Parametricity for Computational Effects.” Logical Methods in Computer Science 5 (3:7): 1–31. https://doi.org/10.2168/LMCS-5(3:7)2009.
Moggi, Eugenio. 1991. “Notions of Computation and Monads.” Information and Computation 93 (1): 55–92. https://doi.org/10.1016/0890-5401(91)90052-4.
Møller, Anders, and Michael I. Schwartzbach. 2025. Static Program Analysis. https://cs.au.dk/~amoeller/spa/.
Moon, Benjamin, Harley Eades III, and Dominic Orchard. 2021. “Graded Modal Dependent Type Theory.” Programming Languages and Systems: 30th European Symposium on Programming (ESOP 2021). https://arxiv.org/abs/2010.13163.
Morris, J. Garrett, and James McKinna. 2019. “Abstracting Extensible Data Types: Or, Rows by Any Other Name.” Proceedings of the ACM on Programming Languages 3 (POPL): 1–28. https://doi.org/10.1145/3290325.
Morris, Peter, Thorsten Altenkirch, and Neil Ghani. 2009. “A Universe of Strictly Positive Families.” International Journal of Foundations of Computer Science 20 (1): 83–107. https://doi.org/10.1142/S0129054109006462.
Morris, Sidney A. 2024. Topology Without Tears. https://www.topologywithouttears.net/.
Motroi, Valeriu, and Ştefan Ciobâcă. 2020. A Typo in the Paterson–Wegman–de Champeaux Algorithm. arXiv:2007.00304v1. https://doi.org/10.48550/arXiv.2007.00304.
Moura, Leonardo de, Jeremy Avigad, Soonho Kong, and Cody Roux. 2015. Elaboration in Dependent Type Theory. https://arxiv.org/abs/1505.04324.
Mycroft, Alan. 1984. “Polymorphic Type Schemes and Recursive Definitions.” International Symposium on Programming, Lecture notes in computer science, vol. 167: 217–28. https://doi.org/10.1007/3-540-12925-1_41.
Nakano, Hiroshi. 2000. “A Modality for Recursion.” Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science.
Nanevski, Aleksandar, Frank Pfenning, and Brigitte Pientka. 2008. “Contextual Modal Type Theory.” ACM Transactions on Computational Logic 9 (3): 23:1–49. https://doi.org/10.1145/1352582.1352591.
Necula, George C. 1997. “Proof-Carrying Code.” Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 106–19. https://doi.org/10.1145/263699.263712.
Nederpelt, Rob, and Herman Geuvers. 2014. Type Theory and Formal Proof: An Introduction. Cambridge University Press. https://doi.org/10.1017/CBO9781139567725.
Neergaard, Peter M oller. n.d. The Size-Change Principle of Termination. https://www.cs.brandeis.edu/~cs117a/size-change-termination.pdf.
Neiger, Gil. 1994. “Set-Linearizability.” Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, 396. https://doi.org/10.1145/197917.198176.
Newman, M. H. A. 1942. “On Theories with a Combinatorial Definition of ‘Equivalence’.” Annals of Mathematics 43 (2): 223–43. https://doi.org/10.2307/1968867.
Ngo, Van Chan, Quentin Carbonneaux, and Jan Hoffmann. 2018. “Bounded Expectations: Resource Analysis for Probabilistic Programs.” Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, 496–512. https://doi.org/10.1145/3192366.3192394.
Nipkow, Tobias. 2026. Programming and Proving in Isabelle/HOL. Isabelle Project. https://isabelle.in.tum.de/doc/prog-prove.pdf.
Nordström, Bengt, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-Löf’s Type Theory: An Introduction. International Series of Monographs on Computer Science 7. Oxford University Press.
Nordström, Bengt, Kent Petersson, and Jan M. Smith. 2000. “Martin-Löf’s Type Theory.” In Handbook of Logic in Computer Science, Volume 5: Algebraic and Logical Structures, edited by Samson Abramsky, Dov M. Gabbay, and Tom S. E. Maibaum. Oxford University Press.
Norell, Ulf. 2007. “Towards a Practical Programming Language Based on Dependent Type Theory.” PhD thesis, Chalmers University of Technology. https://research.chalmers.se/en/publication/46311.
O’Hearn, Peter W. 2003. “On Bunched Typing.” Journal of Functional Programming 13 (4): 747–96. https://doi.org/10.1017/S0956796802004495.
O’Hearn, Peter W. 2007. “Resources, Concurrency, and Local Reasoning.” Theoretical Computer Science 375 (1–3): 271–307. https://doi.org/10.1016/j.tcs.2006.12.035.
O’Hearn, Peter W., and David J. Pym. 1999. “The Logic of Bunched Implications.” Bulletin of Symbolic Logic 5 (2): 215–44. https://doi.org/10.2307/421090.
O’Hearn, Peter W., John C. Reynolds, and Hongseok Yang. 2001. “Local Reasoning about Programs That Alter Data Structures.” Computer Science Logic, Lecture notes in computer science, vol. 2142: 1–19. https://doi.org/10.1007/3-540-44802-0_1.
Odersky, Martin, Olivier Blanvillain, Fengyun Liu, Aggelos Biboudis, Heather Miller, and Sandro Stucki. 2018. “Simplicitly: Foundations and Applications of Implicit Function Types.” Proceedings of the ACM on Programming Languages 2 (POPL): 42:1–29. https://doi.org/10.1145/3158130.
Ohori, Atsushi. 1995. “A Polymorphic Record Calculus and Its Compilation.” ACM Transactions on Programming Languages and Systems 17 (6): 844–95. https://doi.org/10.1145/218570.218572.
Oliva, Paulo. 2006. “Understanding and Using Spector’s Bar Recursive Interpretation of Classical Analysis.” Logical Approaches to Computational Barriers, Lecture notes in computer science, vol. 3988: 423–34. https://doi.org/10.1007/11780342_44.
Oliveira, Bruno C. d. S., Zhiyuan Shi, and João Alpuim. 2016. “Disjoint Intersection Types.” Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. https://doi.org/10.1145/2951913.2951945.
Oliveira Vale, Arthur, Zhong Shao, and Yixuan Chen. 2024. “A Compositional Theory of Linearizability.” Journal of the ACM 71 (2): 14:1–107. https://doi.org/10.1145/3643668.
Orchard, Dominic, Vilem-Benjamin Liepelt, and Harley Eades III. 2019. “Quantitative Program Reasoning with Graded Modal Types.” Proceedings of the ACM on Programming Languages 3 (ICFP): 110:1–30. https://doi.org/10.1145/3341714.
Osera, Peter-Michael, Vilhelm Sjöberg, and Steve Zdancewic. 2012. “Dependent Interoperability.” Proceedings of the 6th Workshop on Programming Languages Meets Program Verification. https://doi.org/10.1145/2103776.2103779.
Otten, Jasper. 2026. Large Sizes for Induction and Coinduction.
Palmgren, Erik. 1998. “On Universes in Type Theory.” In Twenty-Five Years of Constructive Type Theory. https://doi.org/10.1093/oso/9780198501275.003.0012.
Palmgren, Erik. 2014. “Lecture Notes on Type Theory.” Unpublished manuscript.
Palmgren, Erik. 2022. “From Type Theory to Setoids and Back.” Mathematical Structures in Computer Science 32 (10): 1283–312. https://doi.org/10.1017/S0960129521000189.
Panangaden, Prakash, and Vasant Shanbhogue. 1992. “The Expressive Power of Indeterminate Dataflow Primitives.” Information and Computation 98 (1): 99–131. https://doi.org/10.1016/0890-5401(92)90043-F.
Parreaux, Lionel. 2020. “The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy.” Proceedings of the ACM on Programming Languages 4 (ICFP): 124:1–30. https://doi.org/10.1145/3409006.
Parreaux, Lionel, and Chun Yin Chau. 2022. “MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types.” Proceedings of the ACM on Programming Languages 6 (OOPSLA2). https://doi.org/10.1145/3563304.
Pasquali, Fabio. 2014. Remarks on the Tripos to Topos Construction: Extensionality, Comprehensions, Quotients and Cauchy-Complete Objects. https://arxiv.org/abs/1401.7867.
Paterson, Mike S., and Mark N. Wegman. 1978. “Linear Unification.” Journal of Computer and System Sciences 16 (2): 158–67. https://doi.org/10.1016/0022-0000(78)90043-0.
Paulin-Mohring, Christine. 1993. “Inductive Definitions in the System Coq: Rules and Properties.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 664: 328–45. https://doi.org/10.1007/BFb0037116.
Paulin-Mohring, Christine. 1996. “Définitions Inductives En Théorie Des Types d’ordre Supérieur.” Habilitation thesis, Université Claude Bernard Lyon I. https://www.lri.fr/~paulin/PUBLIS/habilitation.ps.gz.
Paulin-Mohring, Christine. 2015. “Introduction to the Calculus of Inductive Constructions.” In All about Proofs, Proofs for All, edited by Bruno Woltzenlogel Paleo and David Delahaye, vol. 55. Studies in Logic. College Publications. https://inria.hal.science/hal-01094195.
Paulino, Arthur, Damiano Testa, Edward Ayers, et al. 2026. Metaprogramming in Lean 4. https://leanprover-community.github.io/lean4-metaprogramming-book/.
Paulson, Lawrence C. 1983. Tactics and Tacticals in Cambridge LCF. UCAM-CL-TR-39. University of Cambridge Computer Laboratory. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-39.pdf.
Paulson, Lawrence C. 1986. “Constructing Recursion Operators in Intuitionistic Type Theory.” Journal of Symbolic Computation 2 (4): 325–55. https://doi.org/10.1016/S0747-7171(86)80002-5.
Paulson, Lawrence C. 1987a. Logic and Computation: Interactive Proof with Cambridge LCF. Vol. 2. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
Paulson, Lawrence C. 1987b. “Rewriting and Simplification.” In Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press. https://doi.org/10.1017/CBO9780511526602.010.
Paulson, Lawrence C. 1987c. “Tactics and Tacticals.” In Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press. https://doi.org/10.1017/CBO9780511526602.009.
Payet, Étienne, David J. Pearce, and Fausto Spoto. 2022. “On the Termination of Borrow Checking in Featherweight Rust.” NASA Formal Methods, Lecture notes in computer science, vol. 13260. https://doi.org/10.1007/978-3-031-06773-0_22.
Pearce, David J. 2021. “A Lightweight Formalism for Reference Lifetimes and Borrowing in Rust.” ACM Transactions on Programming Languages and Systems 43 (1). https://doi.org/10.1145/3443420.
Pearlmutter, Barak A., and Jeffrey Mark Siskind. 2008. “Reverse-Mode AD in a Functional Framework: Lambda the Ultimate Backpropagator.” ACM Transactions on Programming Languages and Systems 30 (2): 7:1–36. https://doi.org/10.1145/1330017.1330018.
Pédrot, Pierre-Marie, and Nicolas Tabareau. 2020. “The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects.” Proceedings of the ACM on Programming Languages 4 (POPL): 58:1–28. https://doi.org/10.1145/3371126.
Perrone, Paolo. 2019. Notes on Category Theory with Examples from Basic Mathematics. https://arxiv.org/abs/1912.10642.
Petricek, Tomas. 2017. “Context-Aware Programming Languages.” PhD thesis, University of Cambridge. https://tomasp.net/academic/theses/coeffects/.
Petricek, Tomas, Dominic Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence. https://tomasp.net/academic/papers/coeffects/.
Petricek, Tomas, Dominic Orchard, and Alan Mycroft. 2014. “Coeffects: A Calculus of Context-Dependent Computation.” Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, 123–35. https://doi.org/10.1145/2628136.2628160.
Pfenning, Frank. 1991. “Unification and Anti-Unification in the Calculus of Constructions.” Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, 74–85. https://www.cs.cmu.edu/~fp/papers/lics91.pdf.
Pfenning, Frank. 1995. “Structural Cut Elimination.” Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science, 156–66. https://doi.org/10.1109/LICS.1995.523257.
Pfenning, Frank. 1999. A Focusing Prover. https://www.cs.cmu.edu/~fp/courses/99-atp/lectures/lecture11.html.
Pfenning, Frank. 2001. “Logical Frameworks.” In Handbook of Automated Reasoning, edited by Alan Robinson and Andrei Voronkov, vol. 2. Elsevier; MIT Press. https://doi.org/10.1016/B978-044450813-3/50017-5.
Pfenning, Frank. 2003. Recursive Types. https://www.cs.cmu.edu/~fp/courses/15312-f03/lectures/13-rectypes.html.
Pfenning, Frank. 2016. Lecture Notes on Focusing. https://www.cs.cmu.edu/~fp/courses/15816-f16/lectures/18-focusing.pdf.
Pfenning, Frank. 2024. Information Flow. https://15316-cmu.github.io/2024/lectures/11-infoflow.pdf.
Pfenning, Frank. 2025a. Law and Order. https://www.cs.cmu.edu/~fp/courses/15417-s25/lectures/11-order.pdf.
Pfenning, Frank. 2025b. Linear Functional Programming. https://www.cs.cmu.edu/~fp/courses/15814-f25/lectures/19-linfun.pdf.
Pfenning, Frank. 2025c. Linear Logic. https://www.cs.cmu.edu/afs/.cs.cmu.edu/Web/People/fp/courses/15814-f25/lectures/18-linlogic.pdf.
Pfenning, Frank. 2025d. Logical Frameworks. https://www.cs.cmu.edu/afs/.cs.cmu.edu/Web/People/fp/courses/15814-f25/lectures/21-twelf.pdf.
Pfenning, Frank. 2025e. Ordered Type Checking. https://www.cs.cmu.edu/~fp/courses/15417-s25/lectures/13-ordcheck.pdf.
Pfenning, Frank, and Christine Paulin-Mohring. 1990. “Inductively Defined Types in the Calculus of Constructions.” Mathematical Foundations of Programming Semantics, Lecture notes in computer science, vol. 442: 209–28. https://doi.org/10.1007/BFb0040259.
Pfenning, Frank, and Carsten Sch"urmann. 1998. Twelf User’s Guide. CMU-CS-98-173. Carnegie Mellon University. https://www.cs.cmu.edu/~twelf/guide/.
Pientka, Brigitte. 2015. Mechanizing Meta-Theory in Beluga. http://complogic.cs.mcgill.ca/beluga/beluga-tutorial.pdf.
Pierce, Benjamin C. 1992. “Bounded Quantification Is Undecidable.” Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA), 305–15. https://doi.org/10.1145/143165.143228.
Piróg, Maciej, Piotr Polesiuk, and Filip Sieczkowski. 2019. “Typed Equivalence of Effect Handlers and Delimited Control.” 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Leibniz international proceedings in informatics, vol. 131: 30:1–16. https://doi.org/10.4230/LIPIcs.FSCD.2019.30.
Piróg, Maciej, Tom Schrijvers, Nicolas Wu, and Mauro Jaskelioff. 2018. Syntax and Semantics for Operations with Scopes. https://doi.org/10.1145/3209108.3209166.
Pitts, Andrew M. 2003. “Nominal Logic, a First Order Theory of Names and Binding.” Information and Computation 186 (2): 165–93. https://doi.org/10.1016/S0890-5401(03)00138-X.
Pitts, Andrew M. 2005. Lectures on Nominal Syntax and Semantics. International Summer School on Applied Semantics. https://www.cl.cam.ac.uk/~amp12/talks/appsem2005/.
Pitts, Andrew M. 2013. Nominal Sets and Their Applications. https://www.cl.cam.ac.uk/teaching/1314/L23/materials.html.
Pitts, Andrew M., Justus Matthiesen, and Jasper Derikx. 2015. “A Dependent Type Theory with Abstractable Names.” Electronic Notes in Theoretical Computer Science 312: 19–50. https://doi.org/10.1016/j.entcs.2015.04.003.
Plotkin, Gordon D. 1977. “LCF Considered as a Programming Language.” Theoretical Computer Science 5 (3): 223–55. https://doi.org/10.1016/0304-3975(77)90044-5.
Plotkin, Gordon D., and Martín Abadi. 1993. “A Logic for Parametric Polymorphism.” In Typed Lambda Calculi and Applications, edited by Marc Bezem and Jan Friso Groote, vol. 664. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/BFb0037118.
Plotkin, Gordon D., and Matija Pretnar. 2013. “Handling Algebraic Effects.” Logical Methods in Computer Science 9 (4). https://doi.org/10.2168/LMCS-9(4:23)2013.
Plotkin, Gordon, and John Power. 2003. Algebraic Operations and Generic Effects. https://homepages.inf.ed.ac.uk/gdp/publications/alg_ops_gen_effects.pdf.
Poiret, Josselin, Gaétan Gilbert, Kenji Maillard, et al. 2025. “All Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants.” Proceedings of the ACM on Programming Languages 9 (POPL): 76:1–34. https://doi.org/10.1145/3704912.
Polesiuk, Piotr. 2025. IxFree: Step-Indexed Logical Relations in Coq. https://github.com/ppolesiuk/IxFree.
Pollack, Robert. 2002. “Dependently Typed Records in Type Theory.” Formal Aspects of Computing 13: 386–402. https://doi.org/10.1007/s001650200018.
Pottier, François. 2003. A Constraint-Based Presentation and Generalization of Rows. INRIA.
Poulsen, Casper Bach, and Cas van der Rest. 2023. Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. https://doi.org/10.1145/3571255.
Pous, Damien. 2026. “String Diagrams for Monoidal Categories, in Rocq.” 17th International Conference on Interactive Theorem Proving, Leibniz international proceedings in informatics, vol. 382: 28:1–20. https://doi.org/10.4230/LIPIcs.ITP.2026.28.
Powell, Thomas Rhidian John. 2013. “On Bar Recursive Interpretations of Analysis.” PhD thesis, Queen Mary University of London.
Pujet, Loïc, Yann Leray, and Nicolas Tabareau. 2025. “Observational Equality Meets CIC.” ACM Transactions on Programming Languages and Systems 47 (2): 1–35. https://doi.org/10.1145/3719342.
Pujet, Loïc, and Nicolas Tabareau. 2022. “Observational Equality: Now for Good.” Proceedings of the ACM on Programming Languages 6 (POPL): 32:1–27. https://doi.org/10.1145/3498693.
Pujet, Loïc, and Nicolas Tabareau. 2023. “Impredicative Observational Equality.” Proceedings of the ACM on Programming Languages 7 (POPL): 2171–96. https://doi.org/10.1145/3571739.
Pujet, Loïc, and Nicolas Tabareau. 2024. “Observational Equality Meets CIC.” Programming Languages and Systems (ESOP 2024), Lecture notes in computer science, vol. 14576: 275–301. https://doi.org/10.1007/978-3-031-57262-3_12.
Pym, David J. n.d. Errata to the Semantics and Proof Theory of the Logic of Bunched Implications. https://www.cs.ucl.ac.uk/staff/D.Pym/BI-monograph-errata.pdf.
Pym, David J., Peter W. O’Hearn, and Hongseok Yang. 2004. “Possible Worlds and Resources: The Semantics of BI.” Theoretical Computer Science 315 (1): 257–305. https://doi.org/10.1016/j.tcs.2003.11.020.
Racket Contributors. 2026. The Racket Reference: Syntax Model, Macros, and Language Construction. https://docs.racket-lang.org/reference/syntax-model.html.
Racordon, Dimitri. 2019. “Revisiting Memory Assignment Semantics in Imperative Programming Languages.” PhD thesis, University of Geneva. https://doi.org/10.13097/archive-ouverte/unige:127105.
Racordon, Dimitri, and Dave Abrahams. 2023. “Borrow Checking Hylo.” International Workshop on Aliasing, Capabilities and Ownership.
Racordon, Dimitri, Denys Shabalin, Daniel Zheng, Dave Abrahams, and Brennan Saeta. 2022. “Implementation Strategies for Mutable Value Semantics.” Journal of Object Technology 21 (2): 2:1–33. https://doi.org/10.5381/jot.2022.21.2.a2.
Radanne, Gabriel, Hannes Saffrich, and Peter Thiemann. 2020. “Kindly Bent to Free Us.” Proceedings of the ACM on Programming Languages 4 (ICFP): 103:1–29. https://doi.org/10.1145/3408985.
Ramalingam, G., Junehwa Song, Leo Joskowicz, and R. E. Miller. 1999. “Solving Systems of Difference Constraints Incrementally.” Algorithmica 23 (3): 261–75. https://doi.org/10.1007/PL00009261.
Rapoport, Marianna. 2019. “A Path to DOT: Formalizing Scala with Dependent Object Types.” PhD thesis, University of Waterloo. http://hdl.handle.net/10012/15322.
Rapoport, Marianna, Ifaz Kabir, Paul He, and Ondřej Lhoták. 2017. “A Simple Soundness Proof for Dependent Object Types.” Proceedings of the ACM on Programming Languages 1 (OOPSLA): 46:1–27. https://doi.org/10.1145/3133870.
Rapoport, Marianna, and Ondřej Lhoták. 2019. “A Path to DOT: Formalizing Fully Path-Dependent Types.” Proceedings of the ACM on Programming Languages 3 (OOPSLA): 145:1–29. https://doi.org/10.1145/3360571.
Reader, Callum, and Alessandro Di Giorgio. 2026. “String Diagrams for Closed Symmetric Monoidal Categories.” 34th EACSL Annual Conference on Computer Science Logic, Leibniz international proceedings in informatics, vol. 363: 12:1–23. https://doi.org/10.4230/LIPIcs.CSL.2026.12.
Reed, Jason. 2009. “Higher-Order Constraint Simplification in Dependent Type Theory.” Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 49–56. https://doi.org/10.1145/1577824.1577832.
Régis-Gianas, Yann, and Didier Rémy. 2011. Compilation of Polymorphic Records: Examination and Solutions. https://gallium.inria.fr/~remy/mpri/2010/partiel-2010-2011.pdf.
Rémy, Didier. 1991. Type Inference for Records in a Natural Extension of ML. RR-1431. Institut National de Recherche en Informatique et en Automatique. https://inria.hal.science/inria-00075129.
Rémy, Didier, and Jérôme Vouillon. n.d. The Object Layer. https://caml.inria.fr/pub/docs/u3-ocaml/ocaml-objects.html.
Rest, Cas van der. 2026. “Reusable Programming Language Components.” PhD thesis, Delft University of Technology. https://doi.org/10.4233/uuid:48c18134-87fd-4d1b-b609-2a9d6e242cc2.
Rest, Cas van der, and Casper Bach. 2026. “Hefty Algebras: Modular Elaboration of Higher-Order Effects.” Journal of Functional Programming 35: e25. https://doi.org/10.1017/S0956796825100142.
Retoré, Christian. 2004. The Logic of Categorial Grammars. https://signes.labri.fr/resources/docs/lcg.pdf.
Reynolds, John C. 1983. “Types, Abstraction and Parametric Polymorphism.” In Information Processing 83: Proceedings of the IFIP 9th World Computer Congress, edited by R. E. A. Mason. North-Holland. https://www.cs.cmu.edu/afs/cs/user/jcr/ftp/typesabpara.pdf.
Reynolds, John C. 1984. “Polymorphism Is Not Set-Theoretic.” In Semantics of Data Types, edited by Gilles Kahn, David B. MacQueen, and Gordon Plotkin, vol. 173. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/3-540-13346-1_7.
Reynolds, John C. 2002. “Separation Logic: A Logic for Shared Mutable Data Structures.” LICS 2002, 55–74. https://doi.org/10.1109/LICS.2002.1029817.
Rieg, Lionel. 2014a. Classical Realizability in Coq. V. 8c6187da3ba58bdbbbdbb9ec091c4aa738820361. Released. https://github.com/coq-contribs/classical-realizability.
Rieg, Lionel. 2014b. “On Forcing and Classical Realizability.” PhD thesis, Université de Lyon. https://www.cs.yale.edu/homes/rieg-lionel/thesis/en.html.
Riehl, Emily. 2016. Category Theory in Context. Dover Publications. https://emilyriehl.github.io/files/context.pdf.
Riehl, Emily. 2024. “On the Infinity-Topos Semantics of Homotopy Type Theory.” Bulletin of the London Mathematical Society 56 (2): 461–517. https://doi.org/10.1112/blms.12997.
Riehl, Emily, and Dominic Verity. 2020. “Infinity Category Theory from Scratch.” Higher Structures 4 (1): 115–67. https://doi.org/10.21136/HS.2020.04.
Rijke, Egbert. 2017a. The Join Construction.
Rijke, Egbert. 2017b. Type-Theoretic Replacement and the n-Truncation. https://homotopytypetheory.org/2017/01/31/type-theoretic-replacement-the-n-truncation/.
Rijke, Egbert. 2018. “Classifying Types: Topics in Synthetic Homotopy Theory.” PhD thesis, Carnegie Mellon University. https://arxiv.org/abs/1906.09435.
Rijke, Egbert. 2025. Introduction to Homotopy Type Theory. Cambridge Studies in Advanced Mathematics 219. Cambridge University Press. https://doi.org/10.1017/9781108933568.
Rocq Development Team. 2026a. Conversion Rules. The Rocq Prover Reference Manual. https://rocq-prover.org/doc/master/refman/language/core/conversion.html.
Rocq Development Team. 2026b. Records. The Rocq Prover Reference Manual. https://rocq-prover.org/doc/master/refman/language/core/records.html.
Román, Mario. 2020. Profunctor Optics and Traversals. https://arxiv.org/abs/2001.08045.
Rompf, Tiark, and Nada Amin. 2016. “Type Soundness for Dependent Object Types (DOT).” Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 624–41. https://doi.org/10.1145/2983990.2984008.
Rompf, Tiark, and Martin Odersky. 2010. “Lightweight Modular Staging: A Pragmatic Approach to Runtime Code Generation and Compiled DSLs.” Proceedings of the Ninth International Conference on Generative Programming and Component Engineering, 127–36. https://doi.org/10.1145/1868294.1868314.
Rondon, Patrick M., Ming Kawaguchi, and Ranjit Jhala. 2008. “Liquid Types.” Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, 159–69. https://doi.org/10.1145/1375581.1375602.
Rosain, Johann, Tomas Díaz, Kenji Maillard, et al. 2025a. Bounded Sort Polymorphism with Elimination Constraints. Anonymous author draft dated 16 September 2025.
Rosain, Johann, Tomas Díaz, Kenji Maillard, et al. 2025b. Bounded Sort Polymorphism with Elimination Constraints: Artifact. https://doi.org/10.5281/zenodo.17588484.
Rosain, Johann, Tomas Díaz, Kenji Maillard, et al. 2026. “Bounded Sort Polymorphism with Elimination Constraints.” Proceedings of the ACM on Programming Languages, ahead of print. https://doi.org/10.1145/3776732.
Rose, Kristoffer Høgsbro. 1996. Explicit Substitution: Tutorial and Survey. LS-96-3. BRICS, Aarhus University.
Rossberg, Andreas, and Derek Dreyer. 2013. “Mixin’ up the ML Module System.” ACM Transactions on Programming Languages and Systems 35 (1): 2:1–84. https://doi.org/10.1145/2450136.2450137.
Saillard, Ronan. 2015. “Rewriting Modulo Beta in the Lambda-Pi-Calculus Modulo.” Proceedings of the Tenth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Electronic proceedings in theoretical computer science, vol. 185: 87–101. https://doi.org/10.4204/EPTCS.185.6.
Schrijvers, Tom, Bruno C. d. S. Oliveira, Philip Wadler, and Koar Marntirosian. 2019. “COCHIS: Stable and Coherent Implicits.” Journal of Functional Programming 29: e3. https://doi.org/10.1017/S0956796818000242.
Schuster, Philipp, Jonathan Immanuel Brachthäuser, Marius Müller, and Klaus Ostermann. 2022. “A Typed Continuation-Passing Translation for Lexical Effect Handlers.” Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 69–83. https://doi.org/10.1145/3519939.3523710.
Selinger, Peter. 2021. Programming in Agda: Universes. Lecture 13. https://www.mathstat.dal.ca/~selinger/agda-lectures/.
Sen, Koushik, Darko Marinov, and Gul Agha. 2005. “CUTE: A Concolic Unit Testing Engine for C.” Proceedings of the 10th European Software Engineering Conference Held Jointly with the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 263–72. https://doi.org/10.1145/1081706.1081750.
Serre, Jean-Pierre. 1949--1950. “Groupes d’homotopie Relatifs. Application Aux Espaces Fibrés.” In Séminaire Henri Cartan, vol. 2. https://www.numdam.org/item/SHC_1949-1950__2__A10_0/.
Setzer, Anton. 1998. “Well-Ordering Proofs for Martin-Löf Type Theory.” Annals of Pure and Applied Logic 92 (2): 113–59. https://doi.org/10.1016/S0168-0072(97)00078-X.
Shulman, Michael. 2011. Localization as an Inductive Definition. https://homotopytypetheory.org/2011/12/06/inductive-localization/.
Shulman, Michael. 2012. All Modalities Are HITs. https://homotopytypetheory.org/2012/11/19/all-modalities-are-hits/.
Shulman, Michael. 2015. Modules for Modalities. https://homotopytypetheory.org/2015/07/05/modules-for-modalities/.
Shulman, Michael. 2022. Towards a Third-Generation HOTT. Three-part seminar, CMU HoTT Seminar, Carnegie Mellon University. https://home.sandiego.edu/~shulman/papers/hott-cmu-day1.pdf.
Shulman, Michael, and contributors. 2026. Narya: A Proof Assistant for Higher-Dimensional Type Theory. Software and documentation. https://github.com/gwaithimirdain/narya.
Siek, Jeremy G. n.d. What Is Gradual Typing? https://jsiek.github.io/home/WhatIsGradualTyping.html.
Siek, Jeremy G., and Walid Taha. 2006. “Gradual Typing for Functional Languages.” Scheme and Functional Programming Workshop, 81–92. https://jsiek.github.io/home/siek06gradual.pdf.
Siek, Jeremy G., Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. “Refined Criteria for Gradual Typing.” 1st Summit on Advances in Programming Languages, Leibniz international proceedings in informatics, vol. 32: 274–93. https://doi.org/10.4230/LIPIcs.SNAPL.2015.274.
Simmons, Robert J. 2014. “Structural Focalization.” ACM Transactions on Computational Logic 15 (3): 21:1–33. https://doi.org/10.1145/2629678.
Sjoberg, Vilhelm. 2015. “A Dependently Typed Language with Nontermination.” PhD thesis, University of Pennsylvania. https://www.cs.yale.edu/homes/vilhelm/papers/thesis.pdf.
Sjöberg, Vilhelm, and Stephanie Weirich. 2015. “Programming up to Congruence.” Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 369–82. https://doi.org/10.1145/2676726.2676974.
Smeding, Tom, and Matthijs Vákár. 2023. Artifact for Efficient CHAD. Zenodo. https://doi.org/10.5281/zenodo.10015321.
Smeding, Tom, and Matthijs Vákár. 2024. “Efficient CHAD.” Proceedings of the ACM on Programming Languages 8 (POPL): 1060–88. https://doi.org/10.1145/3632878.
Smetsers, Sjaak, Erik Barendsen, Marko van Eekelen, and Rinus Plasmeijer. 1994. “Guaranteeing Safe Destructive Updates Through a Type System with Uniqueness Information for Graphs.” In Graph Transformations in Computer Science, vol. 776. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/3-540-57787-4_23.
Smith, Jan M. 1988. “The Independence of Peano’s Fourth Axiom from Martin-löf’s Type Theory Without Universes.” The Journal of Symbolic Logic 53 (3): 840–45. https://doi.org/10.2307/2274575.
Smolka, Gert. 2019. Computational Type Theory and Interactive Theorem Proving with Coq. https://www.ps.uni-saarland.de/~smolka/drafts/icl2019.pdf.
Sojakova, Kristina. 2014. Higher Inductive Types as Homotopy-Initial Algebras. https://arxiv.org/abs/1402.0761.
Soloviev, Sergei, and Zhaohui Luo. 2002. “Coercion Completion and Conservativity in Coercive Subtyping.” Annals of Pure and Applied Logic 113. https://doi.org/10.1016/S0168-0072(01)00063-X.
Sozeau, Matthieu. 2009. “A New Look at Generalized Rewriting in Type Theory.” Journal of Formalized Reasoning 2 (1). https://doi.org/10.6092/issn.1972-5787/1574.
Sozeau, Matthieu, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2019. Coq Coq Correct! Formalization Artifact. Zenodo software archive. https://doi.org/10.5281/zenodo.3544373.
Sozeau, Matthieu, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. 2020. “Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq.” Proceedings of the ACM on Programming Languages 4 (POPL): 8:1–28. https://doi.org/10.1145/3371076.
Spector, Clifford. 1962. “Provably Recursive Functionals of Analysis: A Consistency Proof of Analysis by an Extension of Principles Formulated in Current Intuitionistic Mathematics.” In Recursive Function Theory, edited by J. C. E. Dekker, vol. 5. Proceedings of Symposia in Pure Mathematics. American Mathematical Society.
Spiwack, Arnaud. 2015. Notes on Axiomatising Hurkens’s Paradox. https://arxiv.org/abs/1507.04577.
Statman, Richard. 1979. “Intuitionistic Propositional Logic Is Polynomial-Space Complete.” Theoretical Computer Science 9 (1): 67–72. https://doi.org/10.1016/0304-3975(79)90006-9.
Statman, Richard. 2000. “On the Word Problem for Combinators.” In Rewriting Techniques and Applications, edited by Leo Bachmair, vol. 1833. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/10721975_14.
Staton, Sam. 2019. Probabilistic Programming: Bayesian Non-Parametrics and Semantics. https://www.cs.uoregon.edu/research/summerschool/summer19/topics.php#Staton.
Staton, Sam. 2020. “Probabilistic Programs as Measures.” In Foundations of Probabilistic Programming, edited by Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva. Cambridge University Press. https://www.cs.ox.ac.uk/people/samuel.staton/papers/2020cup-chapter.pdf.
Sterbac, Raphaël, and Jonathan Sterling. 2026a. Fuss-Free Cumulative Universes: Reference Implementation. https://github.com/raphael-sterbac/elaboration-universes.
Sterbac, Raphaël, and Jonathan Sterling. 2026b. Fuss-Free Cumulative Universes: Theory and Practice. https://arxiv.org/abs/2607.11329.
Sterling, Jonathan. 2021. “First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory.” PhD Thesis CMU-CS-21-142. Carnegie Mellon University. https://doi.org/10.5281/zenodo.6990769.
Sterling, Jonathan, and Carlo Angiuli. 2021. “Normalization for Cubical Type Theory.” 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–15. https://doi.org/10.1109/LICS52264.2021.9470719.
Sterling, Jonathan, and Robert Harper. 2018. “Guarded Computational Type Theory.” Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 879–88. https://doi.org/10.1145/3209108.3209153.
Sterling, Jonathan, and Robert Harper. 2021. “Logical Relations as Types: Proof-Relevant Parametricity for Program Modules.” Journal of the ACM 68 (6): 1–47. https://doi.org/10.1145/3474834.
Straßburger, Lutz. 2006. Proof Nets and the Identity of Proofs. https://arxiv.org/abs/cs/0610123.
Streicher, Thomas. 1993. Investigations into Intensional Type Theory.
Streicher, Thomas. 2021. “The Genesis of the Groupoid Model.” Mathematical Structures in Computer Science 31 (9): 1003–5. https://doi.org/10.1017/S0960129520000286.
Strom, Robert E., and Shaula Yemini. 1986. “Typestate: A Programming Language Concept for Enhancing Software Reliability.” IEEE Transactions on Software Engineering SE-12 (1): 157–71. https://doi.org/10.1109/TSE.1986.6312929.
Stucki, Nicolas, Jonathan Immanuel Brachthäuser, and Martin Odersky. 2021. “Multi-Stage Programming with Generative and Analytical Macros.” Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, 110–22. https://doi.org/10.1145/3486609.3487203.
Stump, Aaron. 2017. “The Calculus of Dependent Lambda Eliminations.” Journal of Functional Programming 27: e14. https://doi.org/10.1017/S0956796817000053.
Stump, Aaron, and Christopher Jenkins. 2018. “Syntax and Semantics of Cedille.” CoRR abs/1806.04709.
Svendsen, Kasper, Lars Birkedal, and Aleksandar Nanevski. 2011. “Partiality, State and Dependent Types.” Typed Lambda Calculi and Applications, Lecture notes in computer science, vol. 6690: 198–212. https://doi.org/10.1007/978-3-642-21691-6_17.
Swamy, Nikhil. 2021. F* at OPLSS 2021. Oregon Programming Languages Summer School course materials. https://fstar-lang.org/oplss2021/.
Swamy, Nikhil, Guido Martínez, and Aseem Rastogi. 2026. Proof-Oriented Programming in f*. https://fstar-lang.org/tutorial/book/.
Swift Project. 2017. SE-0176: Enforce Exclusive Access to Memory. https://github.com/swiftlang/swift-evolution/blob/main/proposals/0176-enforce-exclusive-access-to-memory.md.
Tabareau, Nicolas, Éric Tanter, and Matthieu Sozeau. 2021. “The Marriage of Univalence and Parametricity.” Journal of the ACM 68 (1): 5:1–44. https://doi.org/10.1145/3429979.
Taha, Walid, and Tim Sheard. 2000. “MetaML and Multi-Stage Programming with Explicit Annotations.” Theoretical Computer Science 248 (1–2): 211–42. https://doi.org/10.1016/S0304-3975(00)00053-0.
Tait, William W. 1967. “Intensional Interpretations of Functionals of Finite Type i.” Journal of Symbolic Logic 32 (2): 198–212. https://doi.org/10.2307/2271658.
Tan, Jun, and Guannan Wei. 2026. When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-Stage Programming with Let-Insertion. https://doi.org/10.5281/zenodo.21392703.
Tang, Wenhao, Daniel Hillerström, Sam Lindley, and J. Garrett Morris. 2024. “Soundly Handling Linearity.” Proceedings of the ACM on Programming Languages 8 (POPL). https://doi.org/10.1145/3632896.
Tang, Wenhao, and Sam Lindley. 2026. “Rows and Capabilities as Modal Effects.” Proceedings of the ACM on Programming Languages, ahead of print. https://doi.org/10.1145/3776674.
Tang, Wenhao, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, and Anton Lorenzen. 2025. “Modal Effect Types.” Proceedings of the ACM on Programming Languages 9 (OOPSLA1). https://doi.org/10.1145/3720476.
Tao, Terence. 2011. An Introduction to Measure Theory. Vol. 126. Graduate Studies in Mathematics. American Mathematical Society. https://terrytao.wordpress.com/books/an-introduction-to-measure-theory/.
Tasson, Christine. 2016. Probabilistic Full Abstraction. https://www.lip6.fr/Christine.Tasson/doc/recherche/16_compositionality_tasson.pdf.
The Agda Standard Library Contributors. 2026. Indexed Container Modules in the Agda Standard Library. https://github.com/agda/agda-stdlib.
The agda-unimath Community. 2026. Agda-Unimath. Released. https://github.com/UniMath/agda-unimath.
The mathlib Community. 2026. Mathlib: Simplicial Sets and Kan Complexes. https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/AlgebraicTopology/SimplicialSet.
The MetaRocq contributors. 2026. MetaRocq: A Metaprogramming and Verified-Kernel Framework for Rocq. GitHub repository. https://github.com/MetaRocq/metarocq.
The Rocq Development Team. 2026. Hurkens’s Paradox in the Rocq Standard Library. https://github.com/rocq-prover/stdlib/blob/V9.1.0/theories/Logic/Hurkens.v.
The UniMath Community. 2024. Schools on Univalent Mathematics. https://unimath.github.io/Schools/.
Thompson, Simon. 1991. Type Theory and Functional Programming. International Computer Science Series. Addison-Wesley.
Tirore, Dawit, Jesper Bengtson, and Marco Carbone. 2025. “Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction.” European Conference on Object-Oriented Programming, Leibniz international proceedings in informatics, vol. 333: 31:1–30. https://doi.org/10.4230/LIPIcs.ECOOP.2025.31.
Tofte, Mads, Lars Birkedal, Martin Elsman, and Niels Hallenberg. 2004. “A Retrospective on Region-Based Memory Management.” Higher-Order and Symbolic Computation 17: 245–65. https://doi.org/10.1023/B:LISP.0000029446.78563.a4.
Tofte, Mads, and Jean-Pierre Talpin. 1997. “Region-Based Memory Management.” Information and Computation 132 (2): 109–76. https://doi.org/10.1006/inco.1996.2613.
Toninho, Bernardo, Luís Caires, and Frank Pfenning. 2011. “Dependent Session Types via Intuitionistic Linear Type Theory.” Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP 2011), 161–72. https://doi.org/10.1145/2003476.2003499.
Toninho, Bernardo, Luís Caires, and Frank Pfenning. 2021. “A Decade of Dependent Session Types.” Proceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming, 3:1–3. https://doi.org/10.1145/3479394.3479398.
Tuerk, Thomas. 2019. Interactive Theorem Proving Course: HOL4. https://hol-theorem-prover.org/hol-course-print.pdf.
Univalent Foundations Program, The. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Https://homotopytypetheory.org/book.
Urban, Christian, and Stefan Berghofer. 2008. Nominal Isabelle. https://isabelle.in.tum.de/nominal/manual/nominal_datatype_manual.pdf.
Utagawa, Kiki. 2019. Poly-Record-Ml: A Polymorphic Record Calculus. https://github.com/utgwkk/poly-record-ml.
UW PLSE. 2026. One-Hole Contexts. https://uwplse.org/2026/04/07/One-hole-contexts.html.
Vákár, Matthijs. 2015. A Framework for Dependent Types and Effects. https://arxiv.org/abs/1512.08009.
Valiron, Benoît. 2019. Tutorial on Quantum Lambda-Calculus. https://www.lri.fr/~valiron/qs-lambda.pdf.
Valiron, Benoît. 2026. Introduction to Quantum Algorithms and Quantum Programming. https://www.lri.fr/~valiron/qnotes.pdf.
Valliappan, Nachiappan, Fabian Ruch, and Carlos Tomé Cortiñas. 2022a. “Normalization for Fitch-Style Modal Calculi.” Proceedings of the ACM on Programming Languages 6 (ICFP): 772–98. https://doi.org/10.1145/3547649.
Valliappan, Nachiappan, Fabian Ruch, and Carlos Tomé Cortiñas. 2022b. Normalization for Fitch-Style Modal Calculi (Artifact). V. 1.0.2. Released. https://doi.org/10.5281/zenodo.6804159.
Van Horn, David, and Matthew Might. 2012. “Systematic Abstraction of Abstract Machines.” Journal of Functional Programming 22 (4–5): 705–46. https://doi.org/10.1017/S0956796812000238.
Veltri, Niccolò. 2022. “Normalization by Evaluation for the Lambek Calculus.” Proceedings of the Tenth International Conference on Non-Classical Logics: Theory and Applications, Electronic proceedings in theoretical computer science, vol. 358: 102–17. https://doi.org/10.4204/EPTCS.358.8.
Vene, Varmo. 2000. “Categorical Programming with Inductive and Coinductive Types.” PhD thesis, University of Tartu. https://kodu.ut.ee/~varmo/papers/.
Viro, Oleg, Oleg Ivanov, Nikita Netsvetaev, and Viatcheslav Kharlamov. 2008. Elementary Topology: Problem Textbook. American Mathematical Society. https://doi.org/10.1090/mbk/054.
Volpano, Dennis, Cynthia Irvine, and Geoffrey Smith. 1996. “A Sound Type System for Secure Flow Analysis.” Journal of Computer Security 4 (2–3): 167–87. https://doi.org/10.3233/JCS-1996-42-304.
Vries, Edsko de, Rinus Plasmeijer, and David M. Abrahamson. 2008. “Uniqueness Typing Simplified.” Implementation and Application of Functional Languages, Lecture notes in computer science, vol. 5083: 201–18. https://doi.org/10.1007/978-3-540-85373-2_12.
Wadler, Philip. 1989. “Theorems for Free!” Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, 347–59. https://doi.org/10.1145/99370.99404.
Wadler, Philip. 1993. “A Taste of Linear Logic.” Mathematical Foundations of Computer Science 1993, Lecture notes in computer science, vol. 711: 185–210. https://doi.org/10.1007/3-540-57182-5_12.
Wadler, Philip, and Stephen Blott. 1989. “How to Make Ad-Hoc Polymorphism Less Ad Hoc.” Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New York, NY, USA), 60–76. https://doi.org/10.1145/75277.75283.
Wadler, Philip, and Robert Bruce Findler. 2009. “Well-Typed Programs Can’t Be Blamed.” Programming Languages and Systems: 18th European Symposium on Programming, ESOP 2009, Lecture notes in computer science, vol. 5502: 1–16. https://doi.org/10.1007/978-3-642-00590-9_1.
Wagner, Andrew, Olek Gierczak, Brianna Marshall, John M. Li, and Amal Ahmed. 2025. “From Linearity to Borrowing.” Proceedings of the ACM on Programming Languages 9 (OOPSLA2). https://doi.org/10.1145/3764117.
Walker, David, Karl Crary, and Greg Morrisett. 2000. Typed Memory Management in a Calculus of Capabilities. Cornell University. https://www.cs.cornell.edu/talc/papers/capabilities-tr.pdf.
Wand, Mitchell. 1987. “Complete Type Inference for Simple Objects.” Proceedings of the Second Annual Symposium on Logic in Computer Science, 37–44.
Wand, Mitchell. 1988. “Corrigendum: Complete Type Inference for Simple Objects.” Proceedings of the Third Annual Symposium on Logic in Computer Science, 132. https://doi.org/10.1109/LICS.1988.5111.
Wand, Mitchell. 1991. “Type Inference for Record Concatenation and Multiple Inheritance.” Information and Computation 93 (1): 1–15. https://doi.org/10.1016/0890-5401(91)90050-C.
Wei, Guannan, Jun Tan, and Dinghong Zhong. 2026. “Let It Be Optimized: Building Multi-Stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl).” Proceedings of the ACM on Programming Languages 10 (ICFP): 278:1–31. https://doi.org/10.1145/3828676.
Wei, Yuhang. 2024. “Synthetic Homotopy Theory.” Master’s thesis. https://arxiv.org/abs/2409.15693.
Weirich, Stephanie. 2010. Generic Programming with Dependent Types. Spring School on Generic and Indexed Programming. https://www.seas.upenn.edu/~sweirich/ssgip/.
Weirich, Stephanie. 2022. Implementing Dependent Types in Pi-Forall. https://arxiv.org/abs/2207.02129.
Weiss, Aaron, Olek Gierczak, Daniel Patterson, and Amal Ahmed. 2021. Oxide: The Essence of Rust. https://arxiv.org/abs/1903.00982.
Wells, J. B. 1999. “Typability and Type Checking in System F Are Equivalent and Undecidable.” Annals of Pure and Applied Logic 98 (1–3): 111–56. https://doi.org/10.1016/S0168-0072(98)00047-5.
Well-Typed. 2026. Optics: Optics as an Abstract Interface. Released. https://github.com/well-typed/optics.
White, Leo. 2026. Locality and Effect Reflection. https://lpw25.net/papers/popl2026.pdf.
White, Leo, Frédéric Bour, and Jeremy Yallop. 2015. “Modular Implicits.” Electronic Proceedings in Theoretical Computer Science 198: 22–63. https://doi.org/10.4204/EPTCS.198.2.
Williams, Thomas, and Didier Rémy. 2018. “A Principled Approach to Ornamentation in ML.” Proceedings of the ACM on Programming Languages 2 (POPL). https://doi.org/10.1145/3158109.
Wright, Andrew K. 1995. “Simple Imperative Polymorphism.” Lisp and Symbolic Computation 8 (4): 343–55. https://doi.org/10.1007/BF01018828.
Wu, Hanwen, and Hongwei Xi. 2017. “Dependent Session Types.” 28th International Conference on Concurrency Theory (CONCUR 2017), Leibniz international proceedings in informatics, vol. 85: 23:1–23. https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
Wu, Nicolas, Tom Schrijvers, and Ralf Hinze. 2014. “Effect Handlers in Scope.” Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell, 1–12. https://doi.org/10.1145/2633357.2633358.
Xi, Hongwei. 2010. Introduction to Programming in ATS. http://ats-lang.github.io/FROZEN000/DOCUMENT/INT2PROGINATS/.
Xia, Li-yao, Yannick Zakowski, Paul He, et al. 2020. “Interaction Trees: Representing Recursive and Impure Programs in Coq.” Proceedings of the ACM on Programming Languages 4 (POPL): 1–32. https://doi.org/10.1145/3371119.
Xie, Ningning, and Daan Leijen. 2021. “Generalized Evidence Passing for Effect Handlers: Efficient Compilation of Effect Handlers to C.” Proceedings of the ACM on Programming Languages 5 (ICFP): 71:1–30. https://doi.org/10.1145/3473576.
Xie, Ningning, Leo White, Olivier Nicole, and Jeremy Yallop. 2023. “MacoCaml: Staging Composable and Compilable Macros.” Proceedings of the ACM on Programming Languages 7 (ICFP): 209:1–45. https://doi.org/10.1145/3607851.
Yang, Zhixuan et al. 2022. “Structured Handling of Scoped Effects.” Programming Languages and Systems. https://doi.org/10.1007/978-3-030-99336-8_17.
Yokoyama, Tetsuo. 2010. “Reversible Computation and Reversible Programming Languages.” Electronic Notes in Theoretical Computer Science 253 (6): 71–81. https://doi.org/10.1016/j.entcs.2010.02.007.
Yoshida, Nobuko, and Michael Kirkedal Thomsen. 2018. Principles and Practice of Reversible Programming. https://mrg.cs.ox.ac.uk/tutorials/cgo2018/.
Zhang, Yizhou. 2017. Tunnelling Effects for Modularity. https://effect-handlers.org/static/shonan146/tunnelling.pdf.
Zhang, Yizhou, and Andrew C. Myers. 2019a. Abstraction-Safe Effect Handlers via Tunneling. https://doi.org/10.1145/3290318.
Zhang, Yizhou, and Andrew C. Myers. 2019b. Abstraction-Safe Effect Handlers via Tunneling: Technical Report. Cornell University. https://hdl.handle.net/1813/60202.
Zhang, Yizhou, Guido Salvaneschi, and Andrew C. Myers. 2020. Handling Bidirectional Control Flow. https://doi.org/10.1145/3428207.
Ziliani, Beta, and Matthieu Sozeau. 2017. “A Comprehensible Guide to a New Unifier for CIC Including Universe Polymorphism and Overloading.” Journal of Functional Programming 27: e10. https://doi.org/10.1017/S0956796817000028.
Zyuzin, Nikita, and Aleksandar Nanevski. 2021. “Contextual Modal Types for Algebraic Effects and Handlers.” Proceedings of the ACM on Programming Languages 5 (ICFP). https://doi.org/10.1145/3473580.

Search the book

Type to search the local edition.