
TL;DR
This paper introduces a novel concurrent proof net construction for the MALL fragment of Linear Logic, linking it to transactional models in distributed systems, enabling resource-aware reasoning about complex transactions.
Contribution
It presents a new proof net paradigm for MALL and establishes a correspondence with transactional models in distributed systems, enhancing understanding of resource management.
Findings
Proof nets can be constructed incrementally and concurrently.
A correspondence between proof nets and super-ACID transactions is established.
The paradigm offers a resource-conscious approach to modeling distributed transactions.
Abstract
In this work we present a computation paradigm based on a concurrent and incremental construction of proof nets (de-sequentialized or graphical proofs) of the pure multiplicative and additive fragment of Linear Logic, a resources conscious refinement of Classical Logic. Moreover, we set a correspon- dence between this paradigm and those more pragmatic ones inspired to transactional or distributed systems. In particular we show that the construction of additive proof nets can be interpreted as a model for super-ACID (or co-operative) transactions over distributed transactional systems (typi- cally, multi-databases).
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 · Logic, Reasoning, and Knowledge · Distributed systems and fault tolerance
