Multiparty Sessions based on Proof Nets
Dimitris Mostrous (LaSIGE, Faculty of Sciences, University of Lisbon)
TL;DR
This paper introduces a novel approach to modeling multiparty sessions using proof nets interpreted through a term language derived from Solos calculus, incorporating synchronization for non-deterministic behaviors.
Contribution
It extends linear logic proof nets with a synchronization mechanism for multiparty sessions, enabling non-deterministic interactions in a formal setting.
Findings
Successfully models multiparty sessions with synchronization
Enables non-deterministic behaviors in session-based interactions
Provides a conservative extension of linear logic proof nets
Abstract
We interpret Linear Logic Proof Nets in a term language based on Solos calculus. The system includes a synchronisation mechanism, obtained by a conservative extension of the logic, that enables to define non-deterministic behaviours and multiparty sessions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Distributed systems and fault tolerance