School of Mathematics

Search site

Dr Nicola Gambino

Associate Professor
Pure Mathematics

Contact details

Room: 9.15
Tel: +44 (0)113 3435143
Email: n.gambino @ leeds.ac.uk

Keywords

Categorical Logic
Type theory
Computer-assisted proof-checking
Operads
Analytic functors
Polynomial functors
2-categories
Quillen model categories

Research interests

I am a mathematician with research interests in mathematical logic, category theory, and theoretical computer science. Within mathematical logic, I am mainly nterested in type theory. In recent years, my work has focused on Homotopy Type Theory and Univalent Type Theories. Within category theory, I am interested in polynomial and analytic functors, species of structures, operads, Quillen model structures, 2-categories, and the connections between these topics.

Useful links

Home page
AMS MathSciNet (Subscription required)
ArXiv
Google scholar

Publications

Awodey S, Gambino N, Sojakova K Homotopy-initial algebras in type theory Journal of the ACM, 63, 2017
DOI:10.1145/3006383
View abstract

Gambino N, Sattler C The Frobenius condition, right properness, and uniform fibrations Journal of Pure and Applied Algebra, 2016
DOI:10.1016/j.jpaa.2017.02.013
View abstract

Awodey S, Gambino N, Palmgren E Introduction– from type theory and homotopy theory to univalent foundations Mathematical Structures in Computer Science, 25, 1005-1009, 2015
DOI:10.1017/S0960129514000474
View abstract

Gambino N, Kock J Polynomial functors and polynomial monads Mathematical Proceedings of the Cambridge Philosophical Society, 134, 153-192, 2013
DOI:10.1017/S0305004112000394
View abstract

Awodey S; Gambino N; Sojakova K Inductive types in homotopy type theoryProceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, 95-104 2012
DOI:10.1109/LICS.2012.21
View abstract

Gambino N, Fiore TM, Kock J Double adjunctions and free monads Cahiers de Topologie et Géométrie Differentielles Catégoriques, LIII, 242-307, 2012
View abstract

Fiore TM, Gambino N, Kock J Monads in double categories Journal of Pure and Applied Algebra, 215, 1174-1197, 2011
DOI:10.1016/j.jpaa.2010.08.003
View abstract

Gambino N Weighted limits in simplicial homotopy theory Journal of Pure and Applied Algebra, 214, 1193-1199, 2010
DOI:10.1016/j.jpaa.2009.10.006
View abstract

Awodey S, Gambino N, Lumsdaine PL, Warren MA Lawvere-Tierney sheaves in Algebraic Set Theory Journal of Symbolic Logic, 74, 861-890, 2009
DOI:10.2178/jsl/1245158088
View abstract

Gambino N The associated sheaf functor theorem in algebraic set theory Annals of Pure and Applied Logic, 156, 68-77, 2008
DOI:10.1016/j.apal.2008.06.008
View abstract

Gambino N Homotopy limits for 2-categories Mathematical Proceedings of the Cambridge Philosophical Society, 145, 43-63, 2008
DOI:10.1017/S0305004108001266
View abstract

Gambino N, Garner R The identity type weak factorisation theorem Theoretical Computer Science, 409, 94-109, 2008
DOI:10.1016/j.tcs.2008.08.030
View abstract

Fiore M, Gambino N, Hyland M, Wynskel G The Cartesian closed bicategory of generalised species of structures Journal of the London Mathematical Society, 77, 203-220, 2008
DOI:10.1112/jlms/jdm096
View abstract

Gambino N, Schuster P Spatiality for formal topologies Mathematical Structures in Computer Science, 17, 65-80, 2007
DOI:10.1017/S0960129506005810
View abstract

Gambino N, Aczel P The generalised type-theoretic interpretation of constructive set theory Journal of Symbolic Logic, 71, 67-103, 2006
DOI:10.2178/jsl/1140641163
View abstract

Gambino N Heyting-valued interpretations for Constructive Set Theory Annals of Pure and Applied Logic, 137, 164-188, 2006
DOI:10.1016/j.apal.2005.05.021
View abstract

Gambino N Presheaf Models for Constructive Set Theories In From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, 2005
DOI:10.1093/acprof:oso/9780198566519.003.0004
View abstract

Gambino N, Hyland M Wellfounded Trees and Dependent Polynomial Functors Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3085, 210-225, 2004
View abstract

Aczel P, Gambino N Collection principles in dependent type theory Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2277 LNCS, 1-23, 2002
View abstract

Gambino N, Joyal A On operads, bimodules and analytic functors Memoirs of the American Mathematical Society
View abstract