Non-commutativity and MELL in the Calculus of Structures

A Guglielmi, L Strassburger

Research output: Contribution to conferencePaper

63 Citations (Scopus)

Abstract

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
Pages54-68
Number of pages15
Publication statusPublished - Sep 2001
EventComputer Science Logic (CSL) 2001 - Lecture Notes in Computer Science -
Duration: 1 Sep 2001 → …

Conference

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

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

Cite this