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)
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.

Additional Information

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
semantics, context, syntactics, machinery, pediatrics, manganese, equations

Email this document to