Strathprints Home | Open Access | Browse | Search | User area | Copyright | Help | Library Home | SUPrimo

A generic operational metatheory for algebraic effects

Johann, Patricia and Simpson, Alex and Voigtlaender, Janis (2010) A generic operational metatheory for algebraic effects. [Proceedings Paper]

[img]
Preview
PDF - Submitted Version
Download (313Kb) | 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.

    Item type: Proceedings Paper
    ID code: 34343
    Keywords: algebra, operational metatheory, logic models, Electronic computers. Computer science
    Subjects: Science > Mathematics > Electronic computers. Computer science
    Department: Faculty of Science > Computer and Information Sciences
    Related URLs:
      Depositing user: Pure Administrator
      Date Deposited: 12 Nov 2011 10:03
      Last modified: 07 Dec 2013 11:57
      URI: http://strathprints.strath.ac.uk/id/eprint/34343

      Actions (login required)

      View Item

      Fulltext Downloads: