The syntax and semantics of quantitative type theory

Atkey, Robert; (2018) The syntax and semantics of quantitative type theory. In: LICS '18. ACM, New York, pp. 56-65. ISBN 978-1-4503-5583-4 (https://doi.org/10.1145/3209108.3209189)

[thumbnail of Atkey-LICS-2018-The-syntax-and-semantics-of-quantitative-type]
Preview
 Text. Filename: Atkey_LICS_2018_The_syntax_and_semantics_of_quantitative_type.pdf
Accepted Author Manuscript
Download (730kB)| Preview

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.

ORCID iDs

Atkey, Robert ORCID logoORCID: https://orcid.org/0000-0002-4414-5047;
CORE (COnnecting REpositories)