The Syntax and Semantics of Quantitative Type Theory
Author: Robert Atkey
Paper Information
| Title: | The Syntax and Semantics of Quantitative Type Theory |
| Authors: | Robert Atkey |
| Proceedings: | LICS PDF files |
| Editors: | Anuj Dawar and Erich Grädel |
| Keywords: | Type Theory, Linear Logic, Categorical Logic |
| Abstract: | ABSTRACT. We present Quantitative Type Theory, a Type Theory that records usage information for each variable in a judgement, based on a previous system by McBride. The usage information is used to give a realizability semantics using a variant of Linear Combinatory Algebras, refining the usual realizability semantics of Type Theory by accurately tracking resource behaviour. We define the semantics in terms of Quantitative Categories with Families, a novel extension of Categories with Families for modelling resource sensitive type theories. |
| Pages: | 10 |
| Talk: | Jul 11 12:20 (Session 64E) |
| Paper: | ![]() |
