- 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.

- 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, Dependently Typed, TYPES 2019, Oslo, June 2019.