5 papers
On Propositional Dynamic Logic and Concurrency
Matteo Acclavio, Fabrizio Montesi, Marco Peressotti
Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as…
Accompanist: A Runtime for Resilient Choreographic Programming
Viktor Strate Kløvedal, Dan Plyukhin, Marco Peressotti +1
In service-oriented architecture, services coordinate in one of two ways: directly, using point-to-point communication, or indirectly, through an intermediary called the orchestrat…
Type-Based Enforcement of Non-Interference for Choreographic Programming
Marco Bertoni, Saverio Giallorenzo, Marco Peressotti
Choreographies describe distributed protocols from a global viewpoint, enabling correct-by-construction synthesis of local behaviours. We develop a policy-parametric type system th…
Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker
We present a library-level formalisation of Hennessy-Milner Logic (HML) - a foundational logic for labelled transition systems (LTSs) - for the Lean Computer Science Library (CSLib…
A Promising Future: Omission Failures in Choreographic Programming
Eva Graversen, Fabrizio Montesi, Marco Peressotti
Choreographic programming promises a simple approach to the coding of concurrent and distributed systems: write the collective communication behaviour of a system of processes as a…