4 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…
Proof Nets for PiL (Full Version)
Matteo Acclavio, Giulia Manara
We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the Ï-calculus as…
Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
Matteo Acclavio, Giulia Manara, Fabrizio Montesi
We introduce a novel approach to studying properties of processes in the Ï-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between speci…
Proofs as Execution Trees for the Ï-Calculus
Matteo Acclavio, Giulia Manara
In this paper, we establish the foundations of a novel logical framework for the Ï-calculus, based on the deduction-as-computation paradigm. Following the standard proof-theoretic…