The syntax and semantics of quantitative type theory

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

9 Citations (Scopus)
50 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationLICS '18
Subtitle of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9-12, 2018, Oxford, United Kingdom
Place of PublicationNew York
Number of pages10
Publication statusPublished - 9 Jul 2018


  • type theory
  • linear logic
  • linear combinatory algebra

Fingerprint Dive into the research topics of 'The syntax and semantics of quantitative type theory'. Together they form a unique fingerprint.

Cite this