19 citations · 96 across the 34 of their papers we have counts for
3 papers · 1 filter
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…