POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Sun 14 Jan 2024 15:08 - 15:30 at Lovelace Room - Session 3 Chair(s): Hugo Paquet

We want to report on recent and ongoing work into the denotational semantics of shared-state concurrent programming languages with Brookes-style trace semantics. Most of the talk would cover our trace semantics for the Release/Acquire (RA) memory model, a fragment of the C/C++ standard. Developing this semantics required us to re-think the interpretation of Brookes trace-sets, moving away from interrupted executions and towards a game-like/rely-guarantee-like intuition about the interaction of the program with its environment. We would like to present to the GALOP community these results and, time permitting, ongoing work about more general trace semantics for shared state, to facilitate discussion and further directions.

Sun 14 Jan

Displayed time zone: London change

14:00 - 15:30
Session 3GALOP at Lovelace Room
Chair(s): Hugo Paquet LIPN, Université Sorbonne Paris Nord
14:00
45m
Keynote
Compositional Development of Certified System Software
GALOP
Zhong Shao Yale University
14:45
22m
Talk
SSA is Freyd Categories
GALOP
Jad Elkhaleq Ghalayini University of Cambridge
15:08
22m
Talk
A Denotational Approach to Release/Acquire Concurrency
GALOP
Yotam Dvir Tel Aviv University, Ohad Kammar University of Edinburgh, Ori Lahav Tel Aviv University