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 ...

• Type: Conference
• Year: 2009
• Where: CSL
• Authors: Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson
• Keywords: Artificial Intelligence, Computational Effects, CSL 2009, Effect Calculus, Enriched Effect Calculus