Picture of aircraft jet engine

Strathclyde research that powers aerospace engineering...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by University of Strathclyde researchers, including by Strathclyde researchers involved in aerospace engineering and from the Advanced Space Concepts Laboratory - but also other internationally significant research from within the Department of Mechanical & Aerospace Engineering. Discover why Strathclyde is powering international aerospace research...

Strathprints also exposes world leading research from the Faculties of Science, Engineering, Humanities & Social Sciences, and from the Strathclyde Business School.

Discover more...

A generic operational metatheory for algebraic effects

Johann, Patricia and Simpson, Alex and Voigtlaender, Janis (2010) A generic operational metatheory for algebraic effects. In: Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science. ACM Press, pp. 209-218. ISBN 978-0-7695-4114-3

[img]
Preview
PDF
genpar.pdf - Accepted Author Manuscript

Download (321kB) | Preview

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.