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. © 2014 Springer-Verlag.
CITATION STYLE
Brunel, A., Gaboardi, M., Mazza, D., & Zdancewic, S. (2014). A core quantitative coeffect calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8410 LNCS, pp. 351–370). Springer Verlag. https://doi.org/10.1007/978-3-642-54833-8_19
Mendeley helps you to discover research relevant for your work.