FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
The Syntax and Semantics of Quantitative Type Theory

Author: Robert Atkey

Paper Information

Title:The Syntax and Semantics of Quantitative Type Theory
Authors:Robert Atkey
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Type Theory, Linear Logic, Categorical Logic
Abstract:

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.

Pages:10
Talk:Jul 11 12:20 (Session 64E)
Paper: