1 citations · 2 across the 6 of their papers we have counts for
7 papers
Library-Grade Modal Logic
Marianna Girlando, Fabrizio Montesi
Modal logic comprises a broad family of logics to reason about relational structures. The literature presents many such logics, displaying diverse operators, semantics, and applica…
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
Choreographic programming (CP) is a programming paradigm for the correct-by-construction development of concurrent and distributed systems: programmers write the intended overall b…
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…
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…
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…
Better Late Than Never: A Fully Abstract Semantics for Classical Processes
Wen Kokke, Fabrizio Montesi, Marco Peressotti
We present Hypersequent Classical Processes (HCP), a revised interpretation of the "Proofs as Processes" correspondence between linear logic and the π-calculus initially proposed b…