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
Modal Type Theory
π 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