A generic operational metatheory for algebraic effects

Patricia Johann, Alex Simpson, Janis Voigtlaender

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

17 Citations (Scopus)

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.
LanguageEnglish
Title of host publicationProceedings of 25th Annual IEEE Symposium on Logic in Computer Science
Pages209-218
Number of pages10
DOIs
Publication statusPublished - 2010

Fingerprint

Syntactics
Polymorphism
Computer programming languages
Machinery
Semantics

Keywords

  • algebra
  • operational metatheory
  • logic models

Cite this

Johann, P., Simpson, A., & Voigtlaender, J. (2010). A generic operational metatheory for algebraic effects. In Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science (pp. 209-218) https://doi.org/10.1109/LICS.2010.29
Johann, Patricia ; Simpson, Alex ; Voigtlaender, Janis. / A generic operational metatheory for algebraic effects. Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science. 2010. pp. 209-218
@inproceedings{cd5496cf1df8464da9be639f51a5c5c3,
title = "A generic operational metatheory for algebraic effects",
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 contextualpreorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity.",
keywords = "algebra, operational metatheory, logic models",
author = "Patricia Johann and Alex Simpson and Janis Voigtlaender",
year = "2010",
doi = "10.1109/LICS.2010.29",
language = "English",
isbn = "978-0-7695-4114-3",
pages = "209--218",
booktitle = "Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science",

}

Johann, P, Simpson, A & Voigtlaender, J 2010, A generic operational metatheory for algebraic effects. in Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science. pp. 209-218. https://doi.org/10.1109/LICS.2010.29

A generic operational metatheory for algebraic effects. / Johann, Patricia; Simpson, Alex; Voigtlaender, Janis.

Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science. 2010. p. 209-218.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - A generic operational metatheory for algebraic effects

AU - Johann, Patricia

AU - Simpson, Alex

AU - Voigtlaender, Janis

PY - 2010

Y1 - 2010

N2 - 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 contextualpreorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity.

AB - 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 contextualpreorder (hence equivalence) including extensionality properties and a characterisation via applicative contexts, and we provide machinery for reasoning about polymorphism using relational parametricity.

KW - algebra

KW - operational metatheory

KW - logic models

U2 - 10.1109/LICS.2010.29

DO - 10.1109/LICS.2010.29

M3 - Conference contribution book

SN - 978-0-7695-4114-3

SP - 209

EP - 218

BT - Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science

ER -

Johann P, Simpson A, Voigtlaender J. A generic operational metatheory for algebraic effects. In Proceedings of 25th Annual IEEE Symposium on Logic in Computer Science. 2010. p. 209-218 https://doi.org/10.1109/LICS.2010.29