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.
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.
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: Department of Mathematics, University of Manchester,
Alan Turing building, Oxford Road, Manchester M13 9PL, United
Kingdom
Email: nicola.gambino AT manchester DOT ac DOT uk
Web: https://personalpages.manchester.ac.uk/staff/nicola.gambino
Office: Room 2.106.