A Generic Operational Metatheory for Algebraic Effects
- ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
- Patricia Johann Ph.D, Professor (Creator)
- Institution
- Appalachian State University (ASU )
- Web Site: https://library.appstate.edu/
Abstract: We provide a syntactic analysis of contextualpreorder and equivalence for a polymorphic programminglanguage with effects. Our approach applies uniformly acrossa range of algebraic effects, and incorporates, as instances:errors, input/output, global state, nondeterminism, probabilisticchoice, and combinations thereof. Our approach is toextend Plotkin and Power’s structural operational semanticsfor algebraic effects (FoSSaCS 2001) with a primitive “basicpreorder” on ground type computation trees. The basic preorderis used to derive notions of contextual preorder andequivalence on program terms. Under mild assumptions onthis relation, we prove fundamental properties of contextualpreorder (hence equivalence) including extensionality propertiesand a characterization via applicative contexts, and weprovide machinery for reasoning about polymorphism usingrelational parametricity.
A Generic Operational Metatheory for Algebraic Effects
PDF (Portable Document Format)
331 KB
Created on 9/9/2016
Views: 1425
Additional Information
- Publication
- Patricia Johann, Alex Simpson, and Janis Voigtlaender (2010) "A Generic Operational Metatheory for Algebraic Effects". Proceedings, Logic in Computer Science 2010 (LICS'10), pp. 209 - 218. Version Of Record Available From www.ieee.org
- Language: English
- Date: 2010
- Keywords
- semantics, context, syntactics, machinery, pediatrics, manganese, equations