Homotopy Type Theory: Programming and Verification
Lead Research Organisation:
University of Leeds
Department Name: Pure Mathematics
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
People |
ORCID iD |
| Nicola Gambino (Principal Investigator) |
Publications
AWODEY S
(2015)
Introduction - from type theory and homotopy theory to univalent foundations
in Mathematical Structures in Computer Science
Awodey S
(2017)
Homotopy-Initial Algebras in Type Theory
in Journal of the ACM
Fiore M
(2017)
Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures
in Selecta Mathematica
Gambino N
(2017)
The Frobenius condition, right properness, and uniform fibrations
in Journal of Pure and Applied Algebra
Gambino N
(2017)
On operads, bimodules and analytic functors
in Memoirs of the American Mathematical
Society
Gambino N
(2022)
Towards a constructive simplicial model of Univalent Foundations
in Journal of the London Mathematical Society
GAMBINO N
(2021)
MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
in The Journal of Symbolic Logic
Gambino Nicola
(2019)
Models of Martin-Löf type theory from algebraic weak factorisation systems
in arXiv e-prints
Gambino Nicola
(2019)
Towards a constructive simplicial model of Univalent Foundations
in arXiv e-prints
Gambino Nicola
(2019)
The constructive Kan-Quillen model structure: two new proofs
in arXiv e-prints
| Description | My research focuses on new connection between two distant areas of pure mathematics: logic (which studies reasoning) and topology (which studies shapes). The results of my research have improved our understanding of these connections by isolating the essential features that some topological models of the logical systems need to have. This has been done by abstracting away from two known examples (the simplicial and cubical models of type theory), so as to develop a general theory. Further research has focused on obtaining new models of other logical systems using the notion of an operad (which describes a variety of algebraic structures) and on the characterisation of recursive data-types using topological insights. I have also made significant progress towards the solution of one of the key open problems in the area, i.e. the definition of a constructive simplicial model of univalent foundations. |
| Exploitation Route | One of the goals of my research in the long-term is to guide the implementation of new programming languages and of new software-verification tools, to be applied in safety-critical systems. My theoretical work isolates precisely the small sub-problem that needs to be solved in order to get a a constructive simplicial model of univalent foundations. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | http://www1.maths.leeds.ac.uk/~pmtng/ |
| Description | London Mathematical Society Grant Scheme 3 (Joint Research Groups_ |
| Amount | £2,000 (GBP) |
| Organisation | London Mathematical Society |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 10/2015 |
| End | 10/2016 |
| Description | US Air Force Office for Scientific Research (AFOSR) |
| Amount | $359,000 (USD) |
| Funding ID | FA9550-17-1-0290 |
| Organisation | US Air Force European Office of Air Force Research and Development |
| Sector | Public |
| Country | United Kingdom |
| Start | 09/2017 |
| End | 08/2020 |
| Description | Constructive models of univalent type theories in homotopy types |
| Organisation | Chalmers University of Technology |
| Department | Department of Computer Science and Engineering |
| Country | Sweden |
| Sector | Academic/University |
| PI Contribution | Christian Sattler and Nicola Gambino are investigating the possibility of defining models of univalent type theories that combine the advantages of Voevodsky's simplicial model (i.e. of models supporting all homotopy types) and of Coquand's cubical sets (i.e. of being definable in a constructive meta theory). A promising example is that of prismatic sets, already being considered in the homotopy-theoretic literature. |
| Collaborator Contribution | Investigation of known models of univalent type theories, to check if they support homotopy types. |
| Impact | The project involves both mathematical logic, theoretical computer science, algebraic topology and category theory. |
| Start Year | 2017 |
| Description | Kleisli bicategories |
| Organisation | University of Cambridge |
| Department | Department of Biochemistry |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | I have re-started a collaboration with M. Fiore, M. Hyland and G. Winskel on Kleisli bicategories. This has also branched out into a separate project with M. Fiore on the differential lambda-calculus, with the prospect of the submission of an EPSRC grant application. |
| Collaborator Contribution | We wrote a paper accepted for publication in Selecta Mathematica. |
| Impact | The article "Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures" (publications). |
| Start Year | 2016 |
| Title | Coq code proofs |
| Description | The proofs of the results in the paper "Homotopy-initial algebras in type theory" have been fully formalised in the Coq proof assistant. The resulting computer code has been submitted with the paper for publication. |
| Type Of Technology | Software |
| Year Produced | 2015 |
| Open Source License? | Yes |
| Impact | No notable impact. |
| URL | https://github.com/kristinas/hinitiality |