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)

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.

• Share and Export
  

  RDF+XMLBibTeXRIOXX2 XMLRDF+N-TriplesJSONDublin CoreAtomSimple MetadataReferMETSHTML CitationASCII CitationOpenURL ContextObjectEndNoteOpenURL ContextObject in SpanMODSMPEG-21 DIDLEP3 XMLData Cite XMLRIS (EndNote Online, Zotero, Ref manager, etc)RDF+N3Multiline CSV
• Item metadata

  Item type:	Book Section
  ID code:	64031
  Dates:	Date Event 9 July 2018 Published 1 May 2018 Accepted
  Subjects:	Bibliography. Library Science. Information Resources > Library Science. Information Science
  Department:	Faculty of Science > Computer and Information Sciences
  Depositing user:	Pure Administrator
  Date deposited:	14 May 2018 10:55
  Last modified:	21 Apr 2024 02:09
  Related URLs:	Event
  URI:	https://strathprints.strath.ac.uk/id/eprint/64031