Non-commutativity and MELL in the calculus of structures

Alessio Guglielmi; Lutz Straßburger

doi:10.1007/3-540-44802-0_5

Non-commutativity and MELL in the calculus of structures

Alessio Guglielmi
, Lutz Straßburger

Technical University Dresden

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

82 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 noncommutative 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 language	English
Title of host publication	Computer Science Logic
Subtitle of host publication	15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings
Editors	Laurent Fribourg
Publisher	Springer Verlag
Pages	54-68
Number of pages	15
ISBN (Print)	3540425543, 9783540425540
DOIs	https://doi.org/10.1007/3-540-44802-0_5
Publication status	Published - 1 Jan 2001
Externally published	Yes
Event	15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001 - Paris, France Duration: 10 Sept 2001 → 13 Sept 2001

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2142
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001
Country/Territory	France
City	Paris
Period	10/09/01 → 13/09/01

Access to Document

10.1007/3-540-44802-0_5

Cite this

Guglielmi, A., & Straßburger, L. (2001). Non-commutativity and MELL in the calculus of structures. In L. Fribourg (Ed.), Computer Science Logic: 15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings (pp. 54-68). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2142). Springer Verlag. https://doi.org/10.1007/3-540-44802-0_5

Guglielmi, Alessio ; Straßburger, Lutz. / Non-commutativity and MELL in the calculus of structures. Computer Science Logic: 15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings. editor / Laurent Fribourg. Springer Verlag, 2001. pp. 54-68 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{da47e4d676af412f81e7309a157edc7c,

title = "Non-commutativity and MELL in the calculus of structures",

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 noncommutative 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.",

author = "Alessio Guglielmi and Lutz Stra{\ss}burger",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2001.; 15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001 ; Conference date: 10-09-2001 Through 13-09-2001",

year = "2001",

month = jan,

day = "1",

doi = "10.1007/3-540-44802-0\_5",

language = "English",

isbn = "3540425543",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "54--68",

editor = "Laurent Fribourg",

booktitle = "Computer Science Logic",

}

Guglielmi, A & Straßburger, L 2001, Non-commutativity and MELL in the calculus of structures. in L Fribourg (ed.), Computer Science Logic: 15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2142, Springer Verlag, pp. 54-68, 15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001, Paris, France, 10/09/01. https://doi.org/10.1007/3-540-44802-0_5

Non-commutativity and MELL in the calculus of structures. / Guglielmi, Alessio; Straßburger, Lutz.
Computer Science Logic: 15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings. ed. / Laurent Fribourg. Springer Verlag, 2001. p. 54-68 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2142).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Non-commutativity and MELL in the calculus of structures

AU - Guglielmi, Alessio

AU - Straßburger, Lutz

PY - 2001/1/1

Y1 - 2001/1/1

N2 - 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 noncommutative 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.

AB - 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 noncommutative 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.

U2 - 10.1007/3-540-44802-0_5

DO - 10.1007/3-540-44802-0_5

M3 - Conference contribution

AN - SCOPUS:23044529861

SN - 3540425543

SN - 9783540425540

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 54

EP - 68

BT - Computer Science Logic

A2 - Fribourg, Laurent

PB - Springer Verlag

T2 - 15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001

Y2 - 10 September 2001 through 13 September 2001

ER -

Guglielmi A, Straßburger L. Non-commutativity and MELL in the calculus of structures. In Fribourg L, editor, Computer Science Logic: 15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings. Springer Verlag. 2001. p. 54-68. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-44802-0_5

Non-commutativity and MELL in the calculus of structures

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this