A deep quantitative type system

Giulio Guerrieri; Willem Heijltjes; Joseph Paulus

doi:10.4230/LIPIcs.CSL.2021.24

A deep quantitative type system

Giulio Guerrieri, Willem Heijltjes, Joseph Paulus

Rijksuniversiteit Groningen

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

2 Citations (SciVal)

91 Downloads (Pure)

Abstract

We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the “collection calculus”, as a Curry–Howard interpretation of the type system, that embodies these computational properties.

Original language	English
Title of host publication	29th EACSL Annual Conference on Computer Science Logic, CSL 2021
Subtitle of host publication	CSL 2021
Editors	Christel Baier, Jean Goubault-Larrecq
Place of Publication	Dagstuhl, Germany
Publisher	Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages	24:1-24:24
Number of pages	24
Volume	183
Edition	2021
ISBN (Electronic)	9783959771757
ISBN (Print)	978-3-95977-175-7
DOIs	https://doi.org/10.4230/LIPIcs.CSL.2021.24
Publication status	Published - 13 Jan 2021
Event	29th EACSL Annual Conference on Computer Science Logic (CSL 2021) - Lubijana, Slovenia Duration: 25 Jan 2021 → 28 Jan 2021

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Volume	183
ISSN (Print)	1868-8969

Conference

Conference	29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Country/Territory	Slovenia
City	Lubijana
Period	25/01/21 → 28/01/21

Bibliographical note

Funding Information:
This work was supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing.

Publisher Copyright:
© Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus.

Keywords

Deep inference
Intersection types
Lambda-calculus
Resource calculus

ASJC Scopus subject areas

Software

Access to Document

10.4230/LIPIcs.CSL.2021.24Licence: CC BY

diitAccepted author manuscript, 637 KBLicence: CC BY

Cite this

Guerrieri, G., Heijltjes, W., & Paulus, J. (2021). A deep quantitative type system. In C. Baier, & J. Goubault-Larrecq (Eds.), 29th EACSL Annual Conference on Computer Science Logic, CSL 2021: CSL 2021 (2021 ed., Vol. 183, pp. 24:1-24:24). Article 24 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 183). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2021.24

A deep quantitative type system. / Guerrieri, Giulio; Heijltjes, Willem; Paulus, Joseph.
29th EACSL Annual Conference on Computer Science Logic, CSL 2021: CSL 2021. ed. / Christel Baier; Jean Goubault-Larrecq. Vol. 183 2021. ed. Dagstuhl, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021. p. 24:1-24:24 24 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 183).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Guerrieri, G, Heijltjes, W & Paulus, J 2021, A deep quantitative type system. in C Baier & J Goubault-Larrecq (eds), 29th EACSL Annual Conference on Computer Science Logic, CSL 2021: CSL 2021. 2021 edn, vol. 183, 24, Leibniz International Proceedings in Informatics, LIPIcs, vol. 183, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Dagstuhl, Germany, pp. 24:1-24:24, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), Lubijana, Slovenia, 25/01/21. https://doi.org/10.4230/LIPIcs.CSL.2021.24

Guerrieri G, Heijltjes W, Paulus J. A deep quantitative type system. In Baier C, Goubault-Larrecq J, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021: CSL 2021. 2021 ed. Vol. 183. Dagstuhl, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2021. p. 24:1-24:24. 24. (Leibniz International Proceedings in Informatics, LIPIcs). doi: 10.4230/LIPIcs.CSL.2021.24

Guerrieri, Giulio ; Heijltjes, Willem ; Paulus, Joseph. / A deep quantitative type system. 29th EACSL Annual Conference on Computer Science Logic, CSL 2021: CSL 2021. editor / Christel Baier ; Jean Goubault-Larrecq. Vol. 183 2021. ed. Dagstuhl, Germany : Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2021. pp. 24:1-24:24 (Leibniz International Proceedings in Informatics, LIPIcs).

@inproceedings{036982c2585d402192dd6ca611b2c030,

title = "A deep quantitative type system",

abstract = "We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the “collection calculus”, as a Curry–Howard interpretation of the type system, that embodies these computational properties.",

keywords = "Deep inference, Intersection types, Lambda-calculus, Resource calculus",

author = "Giulio Guerrieri and Willem Heijltjes and Joseph Paulus",

note = "Funding Information: This work was supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing. Publisher Copyright: {\textcopyright} Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus.; 29th EACSL Annual Conference on Computer Science Logic (CSL 2021) ; Conference date: 25-01-2021 Through 28-01-2021",

year = "2021",

month = jan,

day = "13",

doi = "10.4230/LIPIcs.CSL.2021.24",

language = "English",

isbn = "978-3-95977-175-7",

volume = "183",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

pages = "24:1--24:24",

editor = "Christel Baier and Jean Goubault-Larrecq",

booktitle = "29th EACSL Annual Conference on Computer Science Logic, CSL 2021",

address = "Germany",

edition = "2021",

}

TY - GEN

T1 - A deep quantitative type system

AU - Guerrieri, Giulio

AU - Heijltjes, Willem

AU - Paulus, Joseph

N1 - Funding Information: This work was supported by EPSRC Project EP/R029121/1 Typed lambda-calculi with sharing and unsharing. Publisher Copyright: © Giulio Guerrieri, Willem B. Heijltjes, and Joseph W.N. Paulus.

PY - 2021/1/13

Y1 - 2021/1/13

N2 - We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the “collection calculus”, as a Curry–Howard interpretation of the type system, that embodies these computational properties.

AB - We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the “collection calculus”, as a Curry–Howard interpretation of the type system, that embodies these computational properties.

KW - Deep inference

KW - Intersection types

KW - Lambda-calculus

KW - Resource calculus

UR - http://www.scopus.com/inward/record.url?scp=85100891679&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2021.24

DO - 10.4230/LIPIcs.CSL.2021.24

M3 - Chapter in a published conference proceeding

SN - 978-3-95977-175-7

VL - 183

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 24:1-24:24

BT - 29th EACSL Annual Conference on Computer Science Logic, CSL 2021

A2 - Baier, Christel

A2 - Goubault-Larrecq, Jean

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

CY - Dagstuhl, Germany

T2 - 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Y2 - 25 January 2021 through 28 January 2021

ER -

A deep quantitative type system

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

A deep quantitative type system

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this