TY - GEN
T1 - A core quantitative coeffect calculus
AU - Brunel, Aloïs
AU - Gaboardi, Marco
AU - Mazza, Damiano
AU - Zdancewic, Steve
PY - 2014/1/1
Y1 - 2014/1/1
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 ℓscript RPCF inspired by a generalized interpretation of the exponential modality. In ℓscript 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 ℓscript RPCF inspired by a generalized interpretation of the exponential modality. In ℓscript 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.
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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 351
EP - 370
BT - 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, Proceedings
PB - Springer Verlag
T2 - 23rd European Symposium on Programming, ESOP 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Y2 - 5 April 2014 through 13 April 2014
ER -