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.

Publications

10 25 50

Studentship Projects

Project Reference Relationship Related To Start End Student Name
EP/N509760/1 01/10/2016 30/09/2021
1974962 Studentship EP/N509760/1 01/10/2017 31/03/2021 James Wood