Rasmus Ejlers Møgelberg ; Sam Staton - Linear usage of state

lmcs:743 - Logical Methods in Computer Science, March 25, 2014, Volume 10, Issue 1 - https://doi.org/10.2168/LMCS-10(1:17)2014
Linear usage of stateArticle

Authors: Rasmus Ejlers Møgelberg ; Sam Staton

    We investigate the phenomenon that "every monad is a linear state monad". We do this by studying a fully-complete state-passing translation from an impure call-by-value language to a new linear type theory: the enriched call-by-value calculus. The results are not specific to store, but can be applied to any computational effect expressible using algebraic operations, even to effects that are not usually thought of as stateful. There is a bijective correspondence between generic effects in the source language and state access operations in the enriched call-by-value calculus. From the perspective of categorical models, the enriched call-by-value calculus suggests a refinement of the traditional Kleisli models of effectful call-by-value languages. The new models can be understood as enriched adjunctions.


    Volume: Volume 10, Issue 1
    Published on: March 25, 2014
    Imported on: August 27, 2012
    Keywords: Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • Mathematical Operational Semantics for Data-Passing Processes; Funder: UK Research and Innovation; Code: EP/E042414/1

    15 Documents citing this article

    Consultation statistics

    This page has been seen 2310 times.
    This article's PDF has been downloaded 534 times.