Inductive types in
Homotopy Type Theory, written with S. Awodey and K.
Sojakova Proceedings of the 2012 27th
Annual ACM/IEEE Symposium on Logic in Computer Science (LICS
2012), pp. 95-104.
The related Coq code is available on here.
Double adjunctions
and free monads, written with T. M. Fiore and J. Kock Cahiers de Topologie et
Geometrie Differentielles Categoriques, LIII (4) 2012,
pp. 242-307.
Monads in double
categories, written with T. M. Fiore and J. Kock Journal of
Pure and Applied Algebra 215 (6) 2011, pp. 1174-1197.
Wellfounded
Trees and Dependent Polynomial Functors, written with M.
Hyland
In S. Berardi and M. Coppo and F. Damiani (editors), Types
for proofs and programs, Lecture Notes in Computer
Science 3085, Springer (2004), pp. 210-225.
Collection
Principles in Dependent Type Theory, written with P. Aczel
In Z. Luo and J. McKinna and R. Pollack (editors), Types
for proofs and programs, Lecture Notes in Computer
Science 2277, Springer (2002), pp. 1-23.
Postal address: School of Mathematics, University of
Leeds, Leeds LS2 9JT, United Kingdom Phone: +44 (0)113 343 51 43 Email: n.gambino AT leeds.ac.uk Web: http://www.maths.leeds.ac.uk/~pmtng Office: Room 9.15, School of Mathematics
This page was last updated on 9th June
2021 by Nicola Gambino.