research-article

Syntax and Semantics of Quantitative Type Theory

Author:

Robert AtkeyAuthors Info & Claims

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 56 - 65

https://doi.org/10.1145/3209108.3209189

Published: 09 July 2018 Publication History

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.

References

[1]

Samson Abramsky. 1996. Retracing Some Paths in Process Algebra. In CONCUR '96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings. 1--17.

Digital Library

[2]

Samson Abramsky. 2005. A structural approach to reversible computation. Theor. Comput. Sci. 347, 3 (2005), 441--464.

Digital Library

[3]

Samson Abramsky, Esfandiar Haghverdi, and Philip J. Scott. 2002. Geometry of Interaction and Linear Combinatory Algebras. Mathematical Structures in Computer Science 12, 5 (2002), 625--665.

Digital Library

[4]

Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundam. Inform. 77, 4 (2007), 397--449. http://content.iospress.com/articles/fundamenta-informaticae/fi77-4-06

Digital Library

[5]

Andrew Barber. 1996. Dual Intuitionistic Linear Logic. Technical Report ECS-LFCS-96-347. LFCS, University of Edinburgh.

[6]

P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers (Lecture Notes in Computer Science), Leszek Pacholski and Jerzy Tiuryn (Eds.), Vol. 933. Springer, 121--135.

Digital Library

[7]

Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program. 23, 5 (2013), 552--593.

[8]

Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems -23rd European Symposium on Programming, ESOP 2014. 351--370.

Digital Library

[9]

Iliano Cervesato and Frank Pfenning. 2002. A Linear Logical Framework. Inf. Comput. 179, 1 (2002), 19--75.

Digital Library

[10]

Valeria de Paiva and Eike Ritter. 2016. Fibrational Modal Type Theory. Electr. Notes Theor. Comput. Sci. 323 (2016), 143--161.

Digital Library

[11]

Peter Dybjer. 1996. Internal Type Theory. In Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers (Lecture Notes in Computer Science), Stefano Berardi and Mario Coppo (Eds.), Vol. 1158. Springer, 120--134.

Digital Library

[12]

Dan R. Ghica. 2007. Geometry of synthesis: a structured approach to VLSI design. In POPL. ACM, 363--375.

Digital Library

[13]

Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014.331-350.

Digital Library

[14]

Jean-Yves Girard. 1987. Linear Logic. Theor. Comp. Sci. 50 (1987), 1--101.

Digital Library

[15]

Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. In Semantics and Logics of Computation. Cambridge University Press, 79--130.

[16]

Naohiko Hoshino. 2007. Linear Realizability. In Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. 420--434.

Digital Library

[17]

Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. 2014. Memoryful geometry of interaction: from coalgebraic components to algebraic effects. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 52:1--52:10.

Digital Library

[18]

Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 17--30.

Digital Library

[19]

Ugo Dal Lago. 2011. A Short Introduction to Implicit Computational Complexity. In Lectures on Logic and Computation -ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011, Selected Lecture Notes (Lecture Notes in Computer Science), Nick Bezhanishvili and Valentin Goranko (Eds.), Vol. 7388. Springer, 89--109.

[20]

Ugo Dal Lago and Martin Hofmann. 2011. Realizability models and implicit complexity. Theor. Comput. Sci. 412, 20 (2011), 2029--2047.

Digital Library

[21]

Daniel R. Licata, Michael Shulman, and Mitchell Riley. 2017. A Fibrational Framework for Substructural and Modal Logics. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK. 25:1--25:22.

[22]

John Longley and Dag Normann. 2015. Higher-Order Computability. Springer.

Digital Library

[23]

Z. Luo and Y. Zhang. 2016. A Linear Dependent Type Theory. In TYPES 2016.

[24]

The Coq development team. 2017. The Coq proof assistant reference manual. Logical Project. http://coq.inria.fr Version 8.6.

[25]

Conor McBride. 2016. I Got Plenty o' Nuttin'. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 207--233.

[26]

Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In TLCA. 344--359.

Digital Library

[27]

Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008 (Lecture Notes in Computer Science), Roberto M. Amadio (Ed.), Vol. 4962. Springer, 350--364.

Digital Library

[28]

Torben A. Mogensen. 1997. Types for 0, 1 or Many Uses. In Implementation of Functional Languages, 9th International Workshop, IFL'97, St. Andrews, Scotland, UK, September 10-12, 1997, Selected Papers (Lecture Notes in Computer Science), Chris Clack, Kevin Hammond, and Antony J. T. Davie (Eds.), Vol. 1467. Springer, 112--122.

Digital Library

[29]

Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2014. Coeffects: a calculus of context-dependent computation. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 123--135.

Digital Library

[30]

Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society, 221--230.

Digital Library

[31]

Dana S. Scott. 1976. Data Types as Lattices. SIAM J. Comput. 5,3 (1976), 522--587.

Digital Library

[32]

Michael Shulman. 2017. Brouwer's fixed-point theorem in real-cohesive homotopy type theory. CoRR abs:1509.07584v3 (2017). https://arxiv.org/abs/1509.07584v3

[33]

Kazushige Terui. 2001. Light Affine Calculus and Polytime Strong Normalization. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. 209--220.

[34]

The Agda Team. 2018. (2018). http://wiki.portal.chalmers.se/agda.

[35]

Matthijs Vákár. 2015. A Categorical Semantics for Linear Logical Frameworks. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015 (Lecture Notes in Computer Science), Andrew M. Pitts (Ed.), Vol. 9034. Springer, 102--116.

Cited By

Ângelo PIgarashi AT. Vasconcelos V(2024)Linear Contextual Metaprogramming and Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.1401(1-10)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.1
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Show More Cited By

Index Terms

Syntax and Semantics of Quantitative Type Theory
1. Theory of computation
  1. Logic
    1. Linear logic
    2. Type theory

Recommendations

A functional programmer's guide to homotopy type theory
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Dependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical ...
2-Dimensional Directed Type Theory

Recent work on higher-dimensional type theory has explored connections between Martin-Lof type theory, higher-dimensional category theory, and homotopy theory. These connections suggest a generalization of dependent type theory to account for ...
A functional programmer's guide to homotopy type theory
ICFP '16

Dependent type theories are functional programming languages with types rich enough to do computer-checked mathematics and software verification. Homotopy type theory is a recent area of work that connects dependent type theory to the mathematical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 2018

960 pages

ISBN:9781450355834

DOI:10.1145/3209108

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

LICS '18

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 9 - 12, 2018

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

56
Total Citations
View Citations
675
Total Downloads

Downloads (Last 12 months)94
Downloads (Last 6 weeks)13

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ângelo PIgarashi AT. Vasconcelos V(2024)Linear Contextual Metaprogramming and Session TypesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.1401(1-10)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.1
Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Hansen TBrady EAlves SCockx J(2024)Type-Level Property Based TestingProceedings of the 9th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3678000.3678206(37-49)Online publication date: 28-Aug-2024
https://dl.acm.org/doi/10.1145/3678000.3678206
Ramsay CStewart RVazou NMorris J(2024)Cloaca: A Concurrent Hardware Garbage Collector for Non-strict Functional LanguagesProceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678277(41-54)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678277
Winterhalter T(2024)Dependent Ghosts Have a Reflection for FreeProceedings of the ACM on Programming Languages10.1145/36746478:ICFP(630-658)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674647
Lorenzen AWhite LDolan SEisenberg RLindley S(2024)Oxidizing OCaml with Modal Memory ManagementProceedings of the ACM on Programming Languages10.1145/36746428:ICFP(485-514)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674642
Buchholtz USchipp von Branitz JSobocinski PLago UEsparza J(2024)Primitive Recursive Dependent Type TheoryProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662136(1-12)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662136
Marshall DOrchard D(2024)Functional Ownership through Fractional UniquenessProceedings of the ACM on Programming Languages10.1145/36498488:OOPSLA1(1040-1070)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649848
Atkey R(2024)Polynomial Time and Dependent TypesProceedings of the ACM on Programming Languages10.1145/36329188:POPL(2288-2317)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632918
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents