| Authors: |
P. Johann, A. Simpson, and J. Voigtländer |
| Published: |
In 25th Symposium on Logic in Computer Science (LICS'10, acceptance rate 40/149), Edinburgh, Scotland, Proceedings, pages 209-218, IEEE, July 2010. |
| DOI: |
10.1109/LICS.2010.29 |
| BibTeX: |
JSV10.bib |
| Abstract: |
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.
|
| Download: |
AGenericOperationalMetatheoryForAlgebraicEffects.pdf |
| Rights: |
Copyright held by IEEE Press. |