Category theory and type theory
Publications
- 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.
The following publications which also appear under Normalization by Evaluation and Inductive and Inductive-Recursive Definitions contain applications of category theory to type theory.
-
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.
Some slides
- 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.