The syntax and semantics of quantitative type theory

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

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.
LanguageEnglish
Title of host publicationLICS '18
Subtitle of host publication33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9--12, 2018, Oxford, United Kingdom
Place of PublicationNew York
Number of pages10
DOIs
StateAccepted/In press - 1 May 2018

Fingerprint

Semantics
Linear algebra
Refining

Keywords

  • type theory
  • linear logic
  • linear combinatory algebra

Cite this

Atkey, R. (Accepted/In press). 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 New York. DOI: 10.1145/3209108.3209189
Atkey, Robert. / The syntax and semantics of quantitative type theory. LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9--12, 2018, Oxford, United Kingdom. New York, 2018.
@inproceedings{3e18689044154c5894c5c8de12a5b581,
title = "The syntax and semantics of quantitative 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.",
keywords = "type theory, linear logic, linear combinatory algebra",
author = "Robert Atkey",
year = "2018",
month = "5",
day = "1",
doi = "10.1145/3209108.3209189",
language = "English",
isbn = "978-1-4503-5583-4",
booktitle = "LICS '18",

}

Atkey, R 2018, 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. New York. DOI: 10.1145/3209108.3209189

The syntax and semantics of quantitative type theory. / Atkey, Robert.

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9--12, 2018, Oxford, United Kingdom. New York, 2018.

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

TY - GEN

T1 - The syntax and semantics of quantitative type theory

AU - Atkey,Robert

PY - 2018/5/1

Y1 - 2018/5/1

N2 - 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.

AB - 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.

KW - type theory

KW - linear logic

KW - linear combinatory algebra

UR - https://lics.siglog.org/lics18/

U2 - 10.1145/3209108.3209189

DO - 10.1145/3209108.3209189

M3 - Conference contribution

SN - 978-1-4503-5583-4

BT - LICS '18

CY - New York

ER -

Atkey R. 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. New York. 2018. Available from, DOI: 10.1145/3209108.3209189