License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2020.23
URN: urn:nbn:de:0030-drops-131804
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13180/
Go to the corresponding LIPIcs Volume Portal

Gordon, Colin S.

Lifting Sequential Effects to Control Operators

pdf-format:
LIPIcs-ECOOP-2020-23.pdf (0.7 MB)

Abstract

Sequential effect systems are a class of effect system that exploits information about program order, rather than discarding it as traditional commutative effect systems do. This extra expressive power allows effect systems to reason about behavior over time, capturing properties such as atomicity, unstructured lock ownership, or even general safety properties. While we now understand the essential denotational (categorical) models fairly well, application of these ideas to real software is hampered by the variety of source level control flow constructs and control operators in real languages.
We address this new problem by appeal to a classic idea: macro-expression of commonly-used programming constructs in terms of control operators. We give an effect system for a subset of Racket’s tagged delimited control operators, as a lifting of an effect system for a language without direct control operators. This gives the first account of sequential effects in the presence of general control operators. Using this system, we also re-derive the sequential effect system rules for control flow constructs previously shown sound directly, and derive sequential effect rules for new constructs not previously studied in the context of source-level sequential effect systems. This offers a way to directly extend source-level support for sequential effect systems to real programming languages.

BibTeX - Entry

@InProceedings{gordon:LIPIcs:2020:13180,
  author =	{Colin S. Gordon},
  title =	{{Lifting Sequential Effects to Control Operators}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{23:1--23:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Robert Hirschfeld and Tobias Pape},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13180},
  URN =		{urn:nbn:de:0030-drops-131804},
  doi =		{10.4230/LIPIcs.ECOOP.2020.23},
  annote =	{Keywords: Type systems, effect systems, quantales, control operators, delimited continuations}
}

Keywords: Type systems, effect systems, quantales, control operators, delimited continuations
Collection: 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Issue Date: 2020
Date of publication: 06.11.2020

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI