| Polynomial functors and polynomial monads N Gambino, J Kock Mathematical proceedings of the cambridge philosophical society 154 (1), 153-192, 2013 | 165 | 2013 |
| The identity type weak factorisation system N Gambino, R Garner Theoretical computer science 409 (1), 94-109, 2008 | 129 | 2008 |
| Wellfounded trees and dependent polynomial functors N Gambino, M Hyland International Workshop on Types for Proofs and Programs, 210-225, 2003 | 127 | 2003 |
| The cartesian closed bicategory of generalised species of structures M Fiore, N Gambino, M Hyland, G Winskel Journal of the London Mathematical Society 77 (1), 203-220, 2008 | 101 | 2008 |
| Inductive types in homotopy type theory S Awodey, N Gambino, K Sojakova 2012 27th Annual IEEE Symposium on Logic in Computer Science, 95-104, 2012 | 54 | 2012 |
| The Frobenius condition, right properness, and uniform fibrations N Gambino, C Sattler Journal of Pure and Applied Algebra 221 (12), 3027-3068, 2017 | 53* | 2017 |
| The generalised type-theoretic interpretation of constructive set theory N Gambino, P Aczel The Journal of Symbolic Logic 71 (1), 67-103, 2006 | 48 | 2006 |
| Weighted limits in simplicial homotopy theory N Gambino Journal of Pure and Applied Algebra 214 (7), 1193-1199, 2010 | 42 | 2010 |
| Heyting-valued interpretations for constructive set theory N Gambino Annals of Pure and Applied Logic 137 (1-3), 164-188, 2006 | 42 | 2006 |
| Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures M Fiore, N Gambino, M Hyland, G Winskel Selecta Mathematica 24 (3), 2791-2830, 2018 | 41* | 2018 |
| Collection principles in dependent type theory P Aczel, N Gambino International Workshop on Types for Proofs and Programs, 1-23, 2000 | 39 | 2000 |
| On operads, bimodules and analytic functors N Gambino, A Joyal Memoirs of the American Mathematical Society 249 (1184), 2017 | 34 | 2017 |
| Spatiality for formal topologies N Gambino, P Schuster Mathematical Structures in Computer Science 17 (1), 65-80, 2007 | 27 | 2007 |
| Presheaf models for constructive set theories N Gambino From sets and types to topology and analysis 48, 62-77, 2005 | 23 | 2005 |
| Sheaf interpretations for generalised predicative intuitionistic systems N Gambino University of Manchester, 2002 | 22 | 2002 |
| Monads in double categories TM Fiore, N Gambino, J Kock Journal of Pure and Applied Algebra 215 (6), 1174-1197, 2011 | 20 | 2011 |
| Towards a constructive simplicial model of Univalent Foundations N Gambino, S Henry Journal of the London Mathematical Society 105 (2), 1073-1109, 2022 | 15 | 2022 |
| Homotopy-initial algebras in type theory S Awodey, N Gambino, K Sojakova Journal of the ACM (JACM) 63 (6), 1-45, 2017 | 14 | 2017 |
| The constructive Kan-Quillen model structure: two new proofs N Gambino, C Sattler, K Szumiło arXiv preprint arXiv:1907.05394, 2019 | 12 | 2019 |
| Lawvere–Tierney sheaves in algebraic set theory S Awodey, N Gambino, PL Lumsdaine, MA Warren The Journal of Symbolic Logic 74 (3), 861-890, 2009 | 10* | 2009 |
Martin HylandProfessor of Mathematical Logic, CambridgeVerified email at dpmms.cam.ac.uk
