Projects per year
Abstract
This article introduces the enriched effect calculus, which extends established type theories for computational effects with primitives from linear logic. The new calculus provides a formalism for expressing linear aspects of computational effects; e.g. the linear usage of imperative features such as state and/or continuations.
The enriched effect calculus is implemented as an extension of a basic effect calculus without linear primitives, which is closely related to Moggi's computational metalanguage, Filinski's effect PCF and Levy's callbypushvalue. We present syntactic results showing: the fidelity of the behaviour of the linear connectives of the enriched effect calculus; the conservativity of the enriched effect calculus over its nonlinear core (the effect calculus); and the nonconservativity of intuitionistic linear logic when considered as an extension of the enriched effect calculus.
The second half of the article investigates models for the enriched effect calculus, based on enriched category theory. We give several examples of such models, relating them to models of standard effect calculi (such as those based on monads), and to models of intuitionistic linear logic. We also prove soundness and completeness.
The enriched effect calculus is implemented as an extension of a basic effect calculus without linear primitives, which is closely related to Moggi's computational metalanguage, Filinski's effect PCF and Levy's callbypushvalue. We present syntactic results showing: the fidelity of the behaviour of the linear connectives of the enriched effect calculus; the conservativity of the enriched effect calculus over its nonlinear core (the effect calculus); and the nonconservativity of intuitionistic linear logic when considered as an extension of the enriched effect calculus.
The second half of the article investigates models for the enriched effect calculus, based on enriched category theory. We give several examples of such models, relating them to models of standard effect calculi (such as those based on monads), and to models of intuitionistic linear logic. We also prove soundness and completeness.
Original language  English 

Journal  Journal of Logic and Computation 
Volume  24 
Issue number  3 
Pages (fromto)  615654 
ISSN  0955792X 
DOIs  
Publication status  Published  2014 
Keywords
 Computational effects
 Linear logic
Fingerprint
Dive into the research topics of 'The Enriched Eﬀect Calculus: Syntax and Semantics'. Together they form a unique fingerprint.Projects
 1 Finished

Modeller og detaljerede kalkuler for eﬀekter i programmeringssprog
Møgelberg, R. E. (CoI)
01/10/2007 → 31/12/2010
Project: Research