APLAS 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Mon 5 Dec 2022 10:30 - 11:00 at Seminar Room G007 - Semantics and Analysis Chair(s): Julian Mackay

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 Abadi and Plotkin’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.

Presentation (Handout) (presentation.pdf)1.53MiB

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Semantics and AnalysisAPLAS at Seminar Room G007
Chair(s): Julian Mackay Victoria University of Wellington
An Algebraic Theory for Shared-State Concurrency
Yotam Dvir Tel Aviv University, Ohad Kammar University of Edinburgh, Ori Lahav Tel Aviv University
File Attached
Decoupling the Ascending and Descending Phases in Abstract Interpretation
Vincenzo Arceri University of Parma, Italy, Isabella Mastroeni University of Verona, Italy, Enea Zaffanella University of Parma, Italy
Inferring Region Types via an Abstract Notion of Environment Transformation
Ulrich Schöpp fortiss GmbH, Chuangjie Xu fortiss GmbH