Semantics for type theories with resource usage annotations

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.