PLDI 2024 (series) / CP 2024 (series) / Choreographic Programming 2024 /
A Propositional Dynamic Logic for Choreographies
This program is tentative and subject to change.
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.
Extended Abstract (CP 2024 - A Propositional Dynamic Logic for Choreographies.pdf) | 323KiB |
This program is tentative and subject to change.
Mon 24 JunDisplayed time zone: Windhoek change
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 20mTalk | 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 20mTalk | Choreographic Programming in Modal Type Theory CP | ||
11:20 20mTalk | 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 20mTalk | Corps: A Core Calculus of Hierarchical Choreographic Programming CP Andrew K. Hirsch University at Buffalo, SUNY Pre-print File Attached | ||
12:00 20mTalk | 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 |