An Algebraic Theory for Shared-State Concurrency

Yotam Dvir*, Ohad Kammar*, Ori Lahav*

*Corresponding author for this work

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

Abstract / Description of output

We present a monadic denotational semantics for a higher-order
programming language with shared-state concurrency,
i.e., global-state in the presence of interleaving concurrency.
Central to our approach is the use of Plotkin and Power's algebraic effect methodology:
designing an equational theory that captures the intended semantics,
and proving a monadic representation theorem for it.
We use Hyland et al.'s equational theory of resumptions that
extends non-deterministic global-state with an operator for yielding to the environment.
The representation is based on Brookes-style traces.
Based on this representation we define a denotational semantics that is
directionally adequate with respect to a standard operational semantics.
We use this semantics to justify compiler transformations of interest:
redundant access eliminations, each following from a mundane algebraic calculation;
while structural transformations follow from reasoning over the monad's interface.
Original languageEnglish
Title of host publicationProgramming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings
EditorsIlya Sergey
PublisherSpringer, Cham
Number of pages22
ISBN (Electronic)978-3-031-21037-2
ISBN (Print)978-3-031-21036-5
Publication statusPublished - 25 Nov 2022
EventAsian Symposium on Programming Languages - University of Auckland, Auckland, New Zealand
Duration: 5 Dec 202210 Dec 2022
Conference number: 20

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Cham
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceAsian Symposium on Programming Languages
Abbreviated titleAPLAS
Country/TerritoryNew Zealand
Internet address

Keywords / Materials (for Non-textual outputs)

  • shared state
  • concurrency
  • denotational semantics
  • monads
  • equational theory
  • program refinement
  • program equivalence
  • compiler transformations
  • compiler optimisations


Dive into the research topics of 'An Algebraic Theory for Shared-State Concurrency'. Together they form a unique fingerprint.

Cite this