5 papers
Choreographic Programming: a Semantic Approach
Matteo Acclavio, Giulia Manara, Fabrizio Montesi +1
The Endpoint Projection (EPP) theorem is a cornerstone of choreographic programming. It states that every choreography can be projected to a network of processes that correctly imp…
Mech: Mechanised Choreographic Programming
Xueying Qin, Marco Peressotti, Fabrizio Montesi
The paper introduces Mech, a Lean 4 mechanisation of choreographic programming that supports general branching, recursion, and nondeterministic choice, and proves soundness and com…
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…
Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
Christopher Henson, Fabrizio Montesi
Following in the footsteps of the success of Mathlib -- the centralised library of formalised mathematics in Lean -- CSLib is a rapidly-growing centralised library of formalised co…
CSLib: The Lean Computer Science Library
Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi +5
We introduce CSLib, an open-source framework for proving computer-science-related theorems and writing formally verified code in the Lean proof assistant. CSLib aims to be for comp…