Non-commutativity and MELL in the Calculus of Structures

A Guglielmi, L Strassburger

Research output: Contribution to conferencePaper

75 Citations (SciVal)


We introduce the calculus of structures: it is more general than the sequent calculus and it allows for cut elimination and the subformula property. We show a simple extension of multiplicative linear logic, by a self-dual non-commutative operator inspired by CCS, that seems not to be expressible in the sequent calculus. Then we show that multiplicative exponential linear logic benefits from its presentation in the calculus of structures, especially because we can replace the ordinary, global promotion rule by a local version. These formal systems, for which we prove cut elimination, outline a range of techniques and properties that were not previously available. Contrarily to what happens in the sequent calculus, the cut elimination proof is modular.
Original languageEnglish
Number of pages15
Publication statusPublished - Sept 2001
EventComputer Science Logic (CSL) 2001 - Lecture Notes in Computer Science -
Duration: 1 Sept 2001 → …


ConferenceComputer Science Logic (CSL) 2001 - Lecture Notes in Computer Science
Period1/09/01 → …


Dive into the research topics of 'Non-commutativity and MELL in the Calculus of Structures'. Together they form a unique fingerprint.

Cite this