Enriching an effect calculus with linear types

Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson

    Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

    Abstract

    We define an ``enriched effect calculus'' by conservatively
    extending  a type theory for
    computational effects
    with primitives from linear logic. By doing so, we obtain
    a generalisation of linear type theory, intended as
    a formalism for expressing linear aspects of effects.

    As a worked example, we formulate  linearly-used continuations
    in the enriched effect calculus. These are captured by a fundamental
    translation of the enriched effect calculus
    into itself, which extends existing call-by-value and call-by-name
    linearly-used CPS translations. We show that our translation is
    involutive. Full completeness results for the various linearly-used
    CPS translations  follow.

    Our main results, the conservativity of enriching the
    effect calculus with linear primitives, and the involution property
    of the fundamental translation, are proved using a category-theoretic
    semantics for the enriched effect calculus. In particular, the involution
    property amounts to the  self-duality of
    the free (syntactic) model.


    Original languageEnglish
    Book seriesLecture Notes in Computer Science
    Volume5771
    Pages (from-to)240
    Number of pages254
    ISSN0302-9743
    DOIs
    Publication statusPublished - 2009
    Event18th EACSL Annual Conference on Computer Science Logic - Coimbra, Portugal
    Duration: 7 Sept 200911 Sept 2009
    Conference number: 18
    http://www.mat.uc.pt/~csl/

    Conference

    Conference18th EACSL Annual Conference on Computer Science Logic
    Number18
    Country/TerritoryPortugal
    CityCoimbra
    Period07/09/200911/09/2009
    Internet address

    Keywords

    • - Enriched Effect Calculus
    • - Linear Logic
    • - Computational Effects
    • - Continuation-Passing Style (CPS) Translation
    • - Category-Theoretic Semantics

    Fingerprint

    Dive into the research topics of 'Enriching an effect calculus with linear types'. Together they form a unique fingerprint.

    Cite this