Some of my Favorite Papers

Parametricity

📄 Robert Atkey, Neil Ghani, and Patricia Johann. 2014. A Relationally Parametric Model of Dependent Type Theory. In Principles of Programming Languages. DOI: https://doi.org/10.1145/2535838.2535852

📄 Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. 2015. A Presheaf Model of Parametric Type Theory. Electron. Notes in Theor. Comput. Sci. 319, (2015), 67–82. DOI: http://dx.doi.org/10.1016/j.entcs.2015.12.006

📕 Guilhem Moulin. 2016. Internalizing Parametricity. phdthesis. Chalmers University of Technology, Sweden. Retrieved from https://publications.lib.chalmers.se/records/fulltext/235758/235758.pdf

📄 Evan Cavallo and Robert Harper. 2021. Internal Parametricity for Cubical Type Theory. Log. Methods Comput. Sci. 17, 4 (2021). DOI: https://doi.org/10.46298/lmcs-17(4:5)2021

📄 Evan Cavallo and Robert Harper. 2020. Internal Parametricity for Cubical Type Theory. In 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, 13:1-13:17. DOI: https://doi.org/10.4230/LIPIcs.CSL.2020.13

Nominal type theory

📄 Ulrich Schöpp and Ian Stark. 2004. A Dependent Type Theory with Names and Binding. In Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings (Lecture Notes in Computer Science), Springer, 235–249. DOI: https://doi.org/10.1007/978-3-540-30124-0\_20

📄 Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In LICS ’01, 221–230. DOI: https://doi.org/10.1109/LICS.2001.932499

📄 Michael Shulman. 2023. Semantics of multimodal adjoint type theory. In Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, Bloomington, IN, USA, June 21-23, 2023 (EPTICS), EpiSciences. DOI: https://doi.org/10.46298/ENTICS.12300

Homotopy Type Theory

📕 Simon Huber. 2016. Cubical Interpretations of Type Theory. phdthesis. University of Gothenburg, Sweden. Retrieved from https://gupea.ub.gu.se/handle/2077/48890

📝 Simon Boulier and Nicolas Tabareau. 2017. Model structure on the universe in a two level type theory. Retrieved from https://hal.archives-ouvertes.fr/hal-01579822

I like the above pre-print better than the published paper (because it contains concepts more readily usable in my own work):

📄 Simon Boulier and Nicolas Tabareau. 2021. Model structure on the universe of all types in interval type theory. Math. Struct. Comput. Sci. 31, 4 (2021), 392–423. DOI: https://doi.org/10.1017/S0960129520000213

Normalization and Conversion

📄 Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. 1995. Categorical Reconstruction of a Reduction Free Normalization Proof. In Category Theory and Computer Science, 6th International Conference, CTCS ’95, Cambridge, UK, August 7-11, 1995, Proceedings (Lecture Notes in Computer Science), Springer, 182–199. DOI: https://doi.org/10.1007/3-540-60164-3\_27

📝 Nathanaëlle Courant and Xavier Leroy. 2025. A Lazy, Concurrent Convertibility Checker. Retrieved from https://arxiv.org/abs/2510.18418

Universal Algebra / Generic Programming Languages Theory

📄 Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. 2021. A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31, (2021), e22. DOI: https://doi.org/10.1017/S0956796820000076

📄 Marcelo Fiore and Dmitrij Szamozvancev. 2022. Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang. 6, POPL (2022), 1–29. DOI: https://doi.org/10.1145/3498715

📕 András Kovács. 2022. Type-Theoretic Signatures for Algebraic Theories and Inductive Types. phdthesis. Eötvös Loránd University, Budapest, Hungary. Retrieved from https://andraskovacs.github.io/pdfs/phdthesis_compact.pdf

Fixpoints in Type Theory

📄 S. Doaitse Swierstra, Marcos Viera, and Atze Dijkstra. 2016. A Lazy Language Needs a Lazy Type System: Introducing Polymorphic Contexts. In Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages (IFL 2016), Association for Computing Machinery, Leuven, Belgium. DOI: https://doi.org/10.1145/3064899.3064906

📄 Daniel Gratzer. 2025. A Modal Deconstruction of Löb Induction. Proc. ACM Program. Lang. 9, POPL, Article 30 (January 2025), 29 pages. https://doi.org/10.1145/3704866