A core quantitative coeffect calculus

Alois Brunel; Marco Gaboardi; Damiano Mazza; Steve Zdancewic

doi:10.1007/978-3-642-54833-8_19

A core quantitative coeffect calculus

Alois Brunel
, Marco Gaboardi
, Damiano Mazza
, Steve Zdancewic

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

66 Citations (Scopus)

Abstract

Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad. Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language lscript RPCF inspired by a generalized interpretation of the exponential modality. In lscript RPCF the exponential modality carries a label - an element of a semiring script R - that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings
Editors	Zhong Shao
Pages	351-370
Number of pages	20
ISBN (Electronic)	9783642548338
DOIs	https://doi.org/10.1007/978-3-642-54833-8_19
Publication status	Published - 2014
Event	23rd European Symposium on Programming - Grenoble, France Duration: 5 Apr 2014 → 13 Apr 2014 http://flint.cs.yale.edu/esop2014/

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	8410
ISSN (Print)	0302-9743

Conference

Conference	23rd European Symposium on Programming
Abbreviated title	ESOP'14
Country/Territory	France
City	Grenoble
Period	5/04/14 → 13/04/14
Internet address	http://flint.cs.yale.edu/esop2014/

Access to Document

10.1007/978-3-642-54833-8_19

Cite this

Brunel, A., Gaboardi, M., Mazza, D., & Zdancewic, S. (2014). A core quantitative coeffect calculus. In Z. Shao (Ed.), Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (pp. 351-370). (Lecture notes in computer science; Vol. 8410). https://doi.org/10.1007/978-3-642-54833-8_19

Brunel, Alois ; Gaboardi, Marco ; Mazza, Damiano et al. / A core quantitative coeffect calculus. Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. editor / Zhong Shao. 2014. pp. 351-370 (Lecture notes in computer science).

@inproceedings{3d5f9f03f4b448efb363bae03ae33a7f,

title = "A core quantitative coeffect calculus",

abstract = "Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad. Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language lscript RPCF inspired by a generalized interpretation of the exponential modality. In lscript RPCF the exponential modality carries a label - an element of a semiring script R - that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis.",

author = "Alois Brunel and Marco Gaboardi and Damiano Mazza and Steve Zdancewic",

year = "2014",

doi = "10.1007/978-3-642-54833-8\_19",

language = "English",

isbn = "9783642548321",

series = "Lecture notes in computer science",

publisher = "Springer ",

pages = "351--370",

editor = "Shao, \{Zhong \}",

booktitle = "Programming Languages and Systems",

note = "23rd European Symposium on Programming, ESOP'14 ; Conference date: 05-04-2014 Through 13-04-2014",

url = "http://flint.cs.yale.edu/esop2014/",

}

Brunel, A, Gaboardi, M, Mazza, D & Zdancewic, S 2014, A core quantitative coeffect calculus. in Z Shao (ed.), Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. Lecture notes in computer science, vol. 8410, pp. 351-370, 23rd European Symposium on Programming, Grenoble, France, 5/04/14. https://doi.org/10.1007/978-3-642-54833-8_19

A core quantitative coeffect calculus. / Brunel, Alois; Gaboardi, Marco; Mazza, Damiano et al.
Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. ed. / Zhong Shao. 2014. p. 351-370 (Lecture notes in computer science; Vol. 8410).

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

TY - GEN

T1 - A core quantitative coeffect calculus

AU - Brunel, Alois

AU - Gaboardi, Marco

AU - Mazza, Damiano

AU - Zdancewic, Steve

PY - 2014

Y1 - 2014

N2 - Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad. Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language lscript RPCF inspired by a generalized interpretation of the exponential modality. In lscript RPCF the exponential modality carries a label - an element of a semiring script R - that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis.

AB - Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad. Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this work, we present a language lscript RPCF inspired by a generalized interpretation of the exponential modality. In lscript RPCF the exponential modality carries a label - an element of a semiring script R - that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis.

UR - https://www.scopus.com/pages/publications/84900549111

U2 - 10.1007/978-3-642-54833-8_19

DO - 10.1007/978-3-642-54833-8_19

M3 - Conference contribution

AN - SCOPUS:84900549111

SN - 9783642548321

T3 - Lecture notes in computer science

SP - 351

EP - 370

BT - Programming Languages and Systems

A2 - Shao, Zhong

T2 - 23rd European Symposium on Programming

Y2 - 5 April 2014 through 13 April 2014

ER -

Brunel A, Gaboardi M, Mazza D, Zdancewic S. A core quantitative coeffect calculus. In Shao Z, editor, Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. 2014. p. 351-370. (Lecture notes in computer science). doi: 10.1007/978-3-642-54833-8_19

A core quantitative coeffect calculus

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this