Enriching an Effect Calculus with Linear Types

9 years 3 months ago
Enriching an Effect Calculus with Linear Types
We define an “enriched effect calculus” by extending a type theory for computational effects with primitives from linear logic. The new calculus, which generalises intuitionistic linear type theory, provides a formalism for expressing linear aspects of computational effects; for example, the linear usage of imperative features such as state and/or continuations. Our main syntactic result is the conservativity of the enriched effect calculus over a basic “effect calculus” without linear primitives (closely related to Moggi’s computational metalanguage, Filinski’s effect PCF and Levy’s call-by-push-value). The proof of this syntactic theorem makes essential use of a category-theoretic semantics, whose study forms the second half of the paper. Our semantic results include soundness, completeness, the initiality of a syntactic model, and an embedding theorem: every model of the basic effect calculus fully embeds in a model of the enriched calculus. The latter means that our ...
Jeff Egger, Rasmus Ejlers Møgelberg, Alex S
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where CSL
Authors Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson
Comments (0)