computer science

Research

My research interests lie at the intersection between mathematical logic and theoretical computer science. The general goal of my work is to advance our understanding of the notion of a constructive proof. This notion can be readily explained by an example: to give a constructive proof of the statement that a differential equation has a solution, we are required to describe an explicit method to define a solution, while to give a non-constructive proof of the same statement we may just show that the assumption of the non-existence of a solution leads to a logical contradiction.

Over the past thirty years, research in mathematical logic and theoretical computer science has increasingly focused on the study of axiomatic systems, called constructive set theories and constructive type theories, which make precise the notion of a constructive proof and its algorithmic content. These systems are not just of theoretical importance, but also of practical utility. For example, constructive type theories are used as the basis for the implementation of computer systems that support the extraction of algorithms from proofs and the design of correct-by-construction programs. These computer systems, in turn, have industrial applications to the verification of safety-critical software.

Keywords:

• Type Theory (dependent type theories, semantics)
• Category Theory (2-dimensional category theory, homotopical algebra)
• Proof Theory (categorical logic, constructive set theory)
• Constructive Mathematics (point-free topology)

Publications

[12] N. Gambino.

Weighted limits in simplicial homotopy theory. Preprint no. 790, Centre de Recerca Matematica (2008). Submitted for publication.

[11] S. Awodey, N. Gambino, P.L. Lumsdaine and M. A. Warren.

Lawvere-Tierney sheaves in Algebraic Set Theory. Journal of Symbolic Logic. Accepted for publication. Forthcoming.

[10] N. Gambino and R. Garner.

The identity type weak factorisation system. Theoretical Computer Science, 409 1 (2008), 94-109.

[9] N. Gambino.

The associated sheaf functor theorem in Algebraic Set Theory. Annals of Pure and Applied Logic, 156 1 (2008), 68-77.

[8] N. Gambino.

Homotopy limits for 2-categories. Mathematical Proceedings of the Cambridge Philosophical Society, 145 1 (2008), 43--63.

[7] M. Fiore, N. Gambino, M. Hyland and G. Winskel.

The cartesian closed bicategory of generalised species of structures. Journal of the London Mathematical Society, 77 2 (2008), 203-220.

[6] N. Gambino and P. Schuster.

Spatiality for formal topologies. Mathematical Structures in Computer Science, 107 1 (2007), 65-80.

[5] N. Gambino.

Heyting-valued interpretations for constructive set theory. Annals of Pure and Applied Logic, 137 1-3 (2006), 164-188.

[4] N. Gambino and P. Aczel.

The generalised type-theoretic interpretation of constructive set theory. Journal of Symbolic Logic, 71 1 (2006), 67-103.

[3] N. Gambino.

Presheaf models for constructive set theories. In L. Crosilla and P. Schuster (editors), From sets and types to topology and analysis, 62-77. Oxford University Press (2005).

[2] N. Gambino and M. Hyland.

Wellfounded trees and dependent polynomial functors. In S. Berardi and M. Coppo and F. Damiani (editors), Types for proofs and programs, 210-225. Lecture Notes in Computer Science 3085, Springer (2004).

[1] P. Aczel and N. Gambino.

Collection principles in dependent type theory. In Z. Luo and J. McKinna and R. Pollack (editors), Types for proofs and programs, 1-23. Lecture Notes in Computer Science 2277, Springer (2002).

Ph.D. thesis

[PhD] N. Gambino.

Sheaf interpretations for generalised predicative intuitionistic systems (2002). Department of Computer Science, University of Manchester. Awarded the annual prize for best doctoral dissertation in the Department of Computer Science in 2003.

Bibtex

Curriculum Vitae

Short Curriculum Vitae

• Oct 2007 - present : Lecturer in Computer Science, University of Leicester.
• Jan 2005 - Jun 2007: Postdoctoral Research Fellow, LaCIM, Universite du Quebec a Montreal.
• Jan 2003 - Dec 2004: EPSRC Postdoctoral Fellow, DPMMS, University of Cambridge.

Full Curriculum Vitae

This is available here

Teaching

• CO1012 Discrete Structures
• CO1001 Logic for Problem Solving

Author: Nicola Gambino (n.gambino@mcs.le.ac.uk), T: +44 (0)116 223 13 04.
© University of Leicester October 29th, 2007 . Last modified: 11th November 2008, 13:33:54.
CS Web Maintainer. Any opinions expressed on this page are those of the author.