The syntax and semantics of quantitative type theory

Robert Atkey

doi:10.1145/3209108.3209189

The syntax and semantics of quantitative type theory

Robert Atkey

Computer And Information Sciences

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

73 Citations (Scopus)

123 Downloads (Pure)

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.

Original language	English
Title of host publication	LICS '18
Subtitle of host publication	Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9-12, 2018, Oxford, United Kingdom
Place of Publication	New York
Pages	56-65
Number of pages	10
DOIs	https://doi.org/10.1145/3209108.3209189
Publication status	Published - 9 Jul 2018

Keywords

type theory
linear logic
linear combinatory algebra

Access to Document

10.1145/3209108.3209189

Atkey-LICS-2018-The-syntax-and-semantics-of-quantitative-typeAccepted author manuscript, 714 KB

Cite this

@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 = jul,

day = "9",

doi = "10.1145/3209108.3209189",

language = "English",

isbn = "978-1-4503-5583-4",

pages = "56--65",

booktitle = "LICS '18",

}

TY - GEN

T1 - The syntax and semantics of quantitative type theory

AU - Atkey, Robert

PY - 2018/7/9

Y1 - 2018/7/9

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 book

SN - 978-1-4503-5583-4

SP - 56

EP - 65

BT - LICS '18

CY - New York

ER -

The syntax and semantics of quantitative type theory

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Bob Atkey