| ||||
| ||||
![]() Title:The Syntax and Semantics of Quantitative Type Theory Authors:Robert Atkey Conference:LICS18 Tags:Categorical Logic, Linear Logic and Type Theory 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. The Syntax and Semantics of Quantitative Type Theory ![]() The Syntax and Semantics of Quantitative Type Theory | ||||
Copyright © 2002 – 2025 EasyChair |