A Sequent Calculus for Modelling Interferences

TL;DR

This paper introduces a new sequent calculus extending linear logic to model interferences, lazy evaluation, and true concurrency, with proven cut-elimination and initial extensions addressing these goals.

Contribution

It presents a conservative extension of linear logic with new connectives for multisequent structures, enabling better modeling of interferences and concurrency in proof search.

Findings

The calculus includes two new connectives for multisequent structures.

It maintains the cut-elimination property.

Initial extensions address modeling interferences and concurrency.

Abstract

A logic calculus is presented that is a conservative extension of linear logic. The motivation beneath this work concerns lazy evaluation, true concurrency and interferences in proof search. The calculus includes two new connectives to deal with multisequent structures and has the cut-elimination property. Extensions are proposed that give first results concerning our objectives.