A core quantitative coeffect calculus

Alois Brunel, Marco Gaboardi, Damiano Mazza, Steve Zdancewic

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    52 Citations (Scopus)


    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 languageEnglish
    Title of host publicationProgramming Languages and Systems
    Subtitle of host publication23rd 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
    EditorsZhong Shao
    Number of pages20
    ISBN (Electronic)9783642548338
    Publication statusPublished - 2014
    Event23rd European Symposium on Programming - Grenoble, France
    Duration: 5 Apr 201413 Apr 2014

    Publication series

    NameLecture notes in computer science
    ISSN (Print)0302-9743


    Conference23rd European Symposium on Programming
    Abbreviated titleESOP'14
    Internet address


    Dive into the research topics of 'A core quantitative coeffect calculus'. Together they form a unique fingerprint.

    Cite this