Sciweavers

LICS
2010
IEEE

A Generic Operational Metatheory for Algebraic Effects

13 years 2 months ago
A Generic Operational Metatheory for Algebraic Effects
—We provide a syntactic analysis of contextual preorder and equivalence for a polymorphic programming language with effects. Our approach applies uniformly across a range of algebraic effects, and incorporates, as instances: errors, input/output, global state, nondeterminism, probabilistic choice, and combinations thereof. Our approach is to extend Plotkin and Power’s structural operational semantics for algebraic effects (FoSSaCS 2001) with a primitive “basic preorder” on ground type computation trees. The basic preorder is used to derive notions of contextual preorder and equivalence on program terms. Under mild assumptions on this relation, we prove fundamental properties of contextual preorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity.
Patricia Johann, Alex Simpson, Janis Voigtlän
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where LICS
Authors Patricia Johann, Alex Simpson, Janis Voigtländer
Comments (0)