BOB ATKEY

The Syntax and Semantics of Quantitative Type Theory

Publication Information

Robert Atkey. The Syntax and Semantics of Quantitative Type Theory. In LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9--12, 2018, Oxford, United Kingdom. 2018.
DOI: 10.1145/3209108.3209189

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.