Semantics for type theories with resource usage annotations
Lead Research Organisation:
University of Strathclyde
Department Name: Computer and Information Sciences
Abstract
Background: We have recently developed a new theory of Quantitative Type Theory. This was strikingly original in that i) it is the first seamless integration of dependent types with intensional information about how terms are computationally represented; ii) it is fully general in being parameterised by any ordered semiring, which allows for a wide range of potential applications: generation of code for low-overhead runtime environments, information flow security enforcement, implicit computational complexity, multistage programming, and distributed programming; and iii) it has a category theoretic semantics which enables rigorous use of the many branches of pure mathematics unified by category theory.
Project Aim: This project will develop the semantics of Quantitative Type Theory to establish general principles for the syntax and semantics of the theory independent of application, developing theories of quantitative data types and their reasoning principles. We will also implement the theory as a type checker to allow for experimentation.
Project Aim: This project will develop the semantics of Quantitative Type Theory to establish general principles for the syntax and semantics of the theory independent of application, developing theories of quantitative data types and their reasoning principles. We will also implement the theory as a type checker to allow for experimentation.
Organisations
People |
ORCID iD |
Neil Ghani (Primary Supervisor) | |
James Wood (Student) |
Publications
Atkey R
(2018)
Context Constrained Computing
Atkey R
(2019)
Linear metatheory via linear algebra
Studentship Projects
Project Reference | Relationship | Related To | Start | End | Student Name |
---|---|---|---|---|---|
EP/N509760/1 | 30/09/2016 | 29/09/2021 | |||
1974962 | Studentship | EP/N509760/1 | 30/09/2017 | 30/07/2021 | James Wood |
EP/R513349/1 | 30/09/2018 | 29/09/2023 | |||
1974962 | Studentship | EP/R513349/1 | 30/09/2017 | 30/07/2021 | James Wood |