Bipolar Proof Nets for MALL

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).