Dr Nicola Gambino

• Mathematical logic (type theory, categorical logic, constructive set theory)
• Category theory (2-categories, model categories, polynomial and analytic functors, operads)
• Theoretical computer Science (computer-assisted proof-checking)

1. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures, with M. Fiore, M. Hyland, and G. Winskel
   Selecta Mathematica - New Series, 24 (3), 2018, pp. 2791-2830
2. The Frobenius condition, right properness, and uniform fibrations, written with C. Sattler
   Journal of Pure and Applied Algebra, 221 (12), 2017, pp. 3027-3068.
   
3.  Homotopy-initial algebras in type theory. written with S. Awodey and K. Sojakova
   Journal of the Association for Computing Machinery, 63 (6), 2017, 45pp.
   
4. On operads, bimodules and analytic functors, written with A. Joyal
   Memoirs of the American Mathematical Society, 249 (1184), 2017, (v) + 110pp.
   
5. Polynomial functors and polynomial monads, written with J. Kock.
   Mathematical Proceedings of the Cambridge Philosophical Society, 154 (1) 2013, pp. 153-192.
   
6. 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.
7. 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.
   
8. Monads in double categories, written with T. M. Fiore and J. Kock
   Journal of Pure and Applied Algebra 215 (6) 2011, pp. 1174-1197.
   
9. Weighted limits in simplicial homotopy theory
   Journal of Pure and Applied Algebra 214 (7) 2010, pp. 1193-1199. 
10. Lawvere-Tierney sheaves in Algebraic Set Theory, written with S. Awodey, P. L. Lumsdaine and M. A. Warren
    Journal of Symbolic Logic 73 (3) 2009, pp. 861-890.
11. The identity type weak factorisation system, with R. Garner
    Theoretical Computer Science 409 (1) 2008, pp. 94-109.
12. The associated sheaf functor theorem in Algebraic Set Theory
    Annals of Pure and Applied Logic 56 (1) 2008, pp. 68-77.
13. Homotopy limits for 2-categories 
    Mathematical Proceedings of the Cambridge Philosophical Society 145 (1) 2008, pp. 43-63.
14. The cartesian closed bicategory of generalised species of structures, written with M. Fiore, M. Hyland and G. Winskel
    Journal of the London Mathematical Society 77 (2) 2008, pp. 203-220. 
15. Spatiality for formal topologies, written with P. Schuster
    Mathematical Structures in Computer Science 17 (1) 2007, pp. 65-80. 
16. Heyting-valued interpretations for constructive set theory
    Annals of Pure and Applied Logic 137 (1-3) 2006, pp. 164-188. 
17. The generalised type-theoretic interpretation of constructive set theory, written with P. Aczel
    Journal of Symbolic Logic 71 (1) 2006, pp. 67-103. 
18. Presheaf models for Constructive Set Theories
    In L. Crosilla and P. Schuster (editors), From Sets and Types to Topology and Analysis, Oxford University Press, 2005, pp. 62-77.
19. 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.
20. 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.

1. On the coherence conditions for pseudo-distributive laws, arXiv:0907:1359, 2009.

• Towards a constructive simplicial model of Univalent Foundations (long version), Mathematical Logic and Constructivity, Stockholm, August 2019.
  
• Towards a constructive simplicial model of Univalent Foundations (short version), International Conference on Homotopy Type Theory 2019, CMU, August 2019
  
• Syntax and semantics of dependent type theories, Summer School on Higher Topos Theory and Univalent Foundations, Leeds, June 2019.
  
• An introduction to CZF,  Seminario de Logica Matematica XXIX #10, Lisbon, January 2018.
• Two talks on algebraic model structures, by Christian Sattler and me, Journées du GDR Topologie Algébrique, Paris, 2016
• Talk I
  
• Talk II
• Algebraic models of homotopy type theory International Category Theory conference, Halifax, 2016.
• Tutorial on Homotopy Type Theory, Young Set Theory, Copenhagen, 2016:
  
• Lecture 1: Type Theory
  
• Lecture 2: Homotopical Algebra
  
• Lecture 3: Homotopical models of type theory
• Lecture 4: Univalent Foundations
• "Aspects of univalence", Homotopy Type Theory and Univalent Foundations at DMV, Hamburg, 2015.
  
• "Univalent foundations of mathematics and homotopical algebra",  Homotopical Algebra and Geometry, Lancaster, 2015.
• A unified approach to Univalent Foundations and Homotopical Algebra, TLCA-RTA, Vienna, July 2014.
• On the bicategory of operads and analytic functors, International Category Theory Conference, Cambridge, 2014.
• Lectures on Homotopy Type Theory, (Dan Licata, Peter LeFanu Lumsdaine and me), Mathematical Structures of Computation, Lyon, 2014.
• The bicategory of operads is cartesian closed, BMC (Special session on Category Theory), Sheffield, 2013.
• An introduction to Homotopy Type Theory, Department of Computer Science seminar, University of Leicester, March 15th, 2013.
  
• Syntax for dependent type theories, Proof Theory and Constructivism Seminar, Leeds, February 20th, 2013.
  
• Il programma "Univalent Foundations of Mathematics" di Vladimir Voevodsky (in Italian), Palermo, May 17th, 2012.
  
• Constructive Mathematics in Constructive Set Theory, Second MALOA Training Workshop, Leeds, June 30th, 2011. 
• Homotopy-theoretic aspects of Martin-Löf type theory, Logic Colloquium 2010, Paris, July 30th, 2010.
• Polynomial Functors and Polynomial Monads, Leeds Symposium in Proof Theory and Constructivism, July 13th 2009.
• Lectures on Dependent Type Theories, Midlands Graduate School 2009, Leicester, March 30th - April 3rd, 2009.

• Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism, Stockholm, August 20th-23rd, 2019
  
• Internation Conference on Homotopy Type Theory 2019, Carnegie Mellon University, Pittsburgh (USA), August 12th-17th, 2019
  
• Summer School on Higher Topos Theory and Univalent Foundations, University of Leeds, June 24th-29th, 2019
  
• YaMCATS (Yorkshire and Midlands Category Theory Seminar).
• 101st Peripatetic Seminar on Sheaves and Logic, Leeds, September 16th-17th, 2017.
• Logic Colloquium 2016, University of Leeds, July 31st-August 6th, 2016.
  
• 96th PSSL, University of Palermo (Italy), celebrating the 60th birthday of Pino Rosolini, 2014.
  
• Type theory, homotopy theory and Univalent Foundations", CRM, Barcelona, 2013.

• Gabriele Lobbia (2018-present).
• Raffael Stenzel, On univalence, Rezk completeness and presentable quasi-categories, 2019.
  
• Marco Larrea, Models of dependent type theory from algebraic weak factorisation systems, 2018.
  
• Jakob Vidmar, Polynomial functors and W-types for groupoids, 2019.
  
• Cesare Gallozzi, Homotopy Type-Theoretic Interpretations of Constructive Set Theories, 2018.
  

• Associate Editor, Mathematical Structures in Computer Science
• Editor, Applied Categorical Structures.

• Homotopical algebra, Graduate course, University of Leeds (2013/14)

• Leeds Logic group webpage
• Leeds Logic seminar