Categorical Combinatorics for Proof Theory and Programming Languages.
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
A long standing problem is to understand semantic models for computer programs, and for mathematical proofs. This is a theoretical problem, spanning the nature of computation, of terminating programs, and convergence, but it has applications as it suggests new ways of using programming languages, new ways of optimizing programs (replacing a program with a semantically identical but faster version), and new ways of verifying program correctness. The research will be published in competitive conferences and journals.
The main aim is to develop a theory of the role that multicategories and enriched categories can play in generalized versions of linear logic. Linearity is crucial in programming languages because it constrains how resources are used. Resources might be memory pointers in conventional programming, or qubits in quantum computing. Categories are a way of giving a theory of equality that is compositional. Theories of equality are important philosophically. But they are also important in practice, for example, they form the basis of optimizing compiler transformations, such as type-directed-partial-evaluation, which make programs run faster. Compositionality is important because it means we can understand a whole program in terms of its parts; again, this is important philosophically, but also in practice, as it allows a compiler to optimize parts of the program.
A secondary aim is to explore concrete and computational formalizations of these semantic structures, in the spirit of the Agda type system, and ongoing 'cubical' extensions of Agda, the Prover9 equational logic prover, and the Globular graphical proof assistant.
The methodology is novel because it builds on recent developments by S Staton and collaborators on categorical models of quantum programming languages using enriched categories and enrichment in combinatorial species (published in MFPS 2017, POPL 2015); on premulticategories and effects (POPL 2013); and possibly on recent work on effect algebras in quantum logic and their relation to presheaf categories (ICALP 2015).
The researcher, Dario Stein, is ideally placed to do this work, because he has taken courses on category theory, quantum computation, combinatorics, algebraic geometry, set theory, logic and decidability in groups, and written a dissertation on locally presentable and accessible categories, as part of his Masters in Mathematics at Cambridge. He is also familiar with more practical aspects of the project, including functional languages (F# and Haskell) and tools (Prover9).
The main aim is to develop a theory of the role that multicategories and enriched categories can play in generalized versions of linear logic. Linearity is crucial in programming languages because it constrains how resources are used. Resources might be memory pointers in conventional programming, or qubits in quantum computing. Categories are a way of giving a theory of equality that is compositional. Theories of equality are important philosophically. But they are also important in practice, for example, they form the basis of optimizing compiler transformations, such as type-directed-partial-evaluation, which make programs run faster. Compositionality is important because it means we can understand a whole program in terms of its parts; again, this is important philosophically, but also in practice, as it allows a compiler to optimize parts of the program.
A secondary aim is to explore concrete and computational formalizations of these semantic structures, in the spirit of the Agda type system, and ongoing 'cubical' extensions of Agda, the Prover9 equational logic prover, and the Globular graphical proof assistant.
The methodology is novel because it builds on recent developments by S Staton and collaborators on categorical models of quantum programming languages using enriched categories and enrichment in combinatorial species (published in MFPS 2017, POPL 2015); on premulticategories and effects (POPL 2013); and possibly on recent work on effect algebras in quantum logic and their relation to presheaf categories (ICALP 2015).
The researcher, Dario Stein, is ideally placed to do this work, because he has taken courses on category theory, quantum computation, combinatorics, algebraic geometry, set theory, logic and decidability in groups, and written a dissertation on locally presentable and accessible categories, as part of his Masters in Mathematics at Cambridge. He is also familiar with more practical aspects of the project, including functional languages (F# and Haskell) and tools (Prover9).
Organisations
People |
ORCID iD |
| Samuel Staton (Primary Supervisor) | |
| Dario Stein (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509711/1 | 01/10/2016 | 30/09/2021 | |||
| 1894512 | Studentship | EP/N509711/1 | 01/10/2017 | 30/09/2020 | Dario Stein |