Category theory and type theory

• Category theory and programming language semantics: an overview. In Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 165--181. Springer-Verlag, 1986.
• Implementing a category of sets in ALF (with Veronica Gaspes), manuscript, 1993.
• Internal type theory, pp 120-134 in TYPES '95, LNCS 1158, 1996.
• Towards formalizing categorical models of type theory in type theory (with Alexandre Buisse), Electronic Notes in Theoretical Computer Science Volume 196, 22 January 2008, Pages 137-151. Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2007). Elsevier.
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory. FLOPS 2008: 3-13 (with Andreas Abel and Thierry Coquand)
• The interpretation of intuitionistic type theory in locally cartesian closed categories - an intuitionistic perspective (with Alexandre Buisse), in Proceedings of MFPS XXIV, Philadelphia 2008. Electr. Notes Theor. Comput. Sci. 218: 21-32 (2008).
• The biequivalence of locally cartesian closed categories and Martin-Lof type theories (with Pierre Clairambault), in Proceedings of TLCA, Novi Sad 2011. Springer LNCS.
• The biequivalence of locally cartesian closed categories and Martin-Lof type theories (with Pierre Clairambault). Mathematical Structures in Computer Science 24(6) (2014).
• Undecidability of Equality in the Free Locally Cartesian Closed Category (with Simon Castellan and Pierre Clairambault). Typed Lambda Calculus and Applications 2015: 138-152.
• Undecidability of Equality in the Free Locally Cartesian Closed Category (extended version) (with Simon Castellan and Pierre Clairambault). Logical Methods in Computer Science 13(4) (2017).
• Categories with Families, Unityped, Simply Typed, Dependently Typed (with Simon Castellan and Pierre Clairambault). ArXiv:1904.00827 [cs.LO], April 2019. To appear in Joachim Lambek: the interplay of mathematics, logic, and linguistics, editors Claudia Casadio and Philip J. Scott, Springer 2021. in
• A Note on Generalized Algebraic Theories and Categories with Families (with Marc Bezem, Thierry Coquand, and Martin Escardo), arXiv:2012.08370, December 2020.

• Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids (with Ilya Beylin). pp 47-61 in TYPES '95, LNCS 1158, 1996.
• A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem (with Sten Agerholm and Ilya Beylin), pp 17-32 in Theorem Proving in Higher Order Logics, editors J. von Wright, J. Grundy, J. Harrison, LNCS 1125, August 1996.
• Normalization and the Yoneda embedding. (with Djordje Cubric and Phil Scott). Mathematical Structures in Computer Science (1998), vol 8, pp 153-192.
• Induction-recursion and initial algebras (with Anton Setzer). Annals of Pure and Applied Logic 124 (2003) 1-47.

• Normalization and the Yoneda Embedding, 7th Scandinavian Logic Symposium, Uppsala, August 1996. (Slightly extended version presented at the LOGSEM workshop, Birmingham, September 1996.)
• A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem, TPHOL, Turku, August 1996.
• Categories with Families: Unityped, Simply Typed, and Dependently Typed, Workshop on Foundations and Applications of Univalent Mathematics, Herrsching, Germany, 18-20 December 2019.