PLDI 2024
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark
Mon 24 Jun 2024 10:40 - 11:00 at Finland - Theory & Verification Chair(s): Saverio Giallorenzo

A Propositional Dynamic Logic for ChoreographiesDynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that the operational semantics for programs considered in these logics is tailored on trace reasoning for sequential programs.

In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL) in which we are able to reason on sets of programs provided with arbitrary operational semantics. We prove cut-elimination and adequacy of a sequent calculus for PDL and we extend these results to OPDL. We conclude by discussing OPDL for Choreographic Programming.

Mon 24 Jun

Displayed time zone: Windhoek change

10:40 - 12:20
Theory & VerificationCP at Finland
Chair(s): Saverio Giallorenzo Alma Mater Studiorum - Università di Bologna / INRIA
10:40
20m
Talk
A Propositional Dynamic Logic for Choreographies
CP
Matteo Acclavio University of Sussex, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark
Pre-print File Attached
11:00
20m
Talk
Choreographic Programming in Modal Type Theory
CP
11:20
20m
Talk
Choreographies meet Communication Failures
CP
Eva Graversen University of Southern Denmark, Fabrizio Montesi University of Southern Denmark, Marco Peressotti University of Southern Denmark
11:40
20m
Talk
Corps: A Core Calculus of Hierarchical Choreographic Programming
CP
Andrew K. Hirsch University at Buffalo, SUNY
Pre-print File Attached
12:00
20m
Talk
Masquerade: Information Flow Control for Choreographies
CP
Michael Piskozub University at Buffalo, SUNY, Ethan Cecchetti University of Wisconsin-Madison, Andrew K. Hirsch University at Buffalo, SUNY