Projects per year
Abstract / Description of output
We present a monadic denotational semantics for a higherorder
programming language with sharedstate concurrency,
i.e., globalstate 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 nondeterministic globalstate with an operator for yielding to the environment.
The representation is based on Brookesstyle 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.
programming language with sharedstate concurrency,
i.e., globalstate 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 nondeterministic globalstate with an operator for yielding to the environment.
The representation is based on Brookesstyle 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 language  English 

Title of host publication  Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings 
Editors  Ilya Sergey 
Publisher  Springer, Cham 
Pages  224 
Number of pages  22 
ISBN (Electronic)  9783031210372 
ISBN (Print)  9783031210365 
DOIs  
Publication status  Published  25 Nov 2022 
Event  Asian Symposium on Programming Languages  University of Auckland, Auckland, New Zealand Duration: 5 Dec 2022 → 10 Dec 2022 Conference number: 20 https://conf.researchr.org/home/aplas2022 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer Cham 
Volume  13658 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Conference
Conference  Asian Symposium on Programming Languages 

Abbreviated title  APLAS 
Country/Territory  New Zealand 
City  Auckland 
Period  5/12/22 → 10/12/22 
Internet address 
Keywords / Materials (for Nontextual outputs)
 shared state
 concurrency
 denotational semantics
 monads
 equational theory
 program refinement
 program equivalence
 compiler transformations
 compiler optimisations
Fingerprint
Dive into the research topics of 'An Algebraic Theory for SharedState Concurrency'. Together they form a unique fingerprint.Projects
 1 Finished

Effectful theories of programming languages: mathematically structured programming
1/12/21 → 31/12/23
Project: Research