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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

82 Citations (Scopus)

Résumé

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.

langue originale	Anglais
titre	Computer Science Logic
Sous-titre	15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings
rédacteurs en chef	Laurent Fribourg
Editeur	Springer Verlag
Pages	54-68
Nombre de pages	15
ISBN (imprimé)	3540425543, 9783540425540
Les DOIs	https://doi.org/10.1007/3-540-44802-0_5
état	Publié - 1 janv. 2001
Modification externe	Oui
Evénement	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 Durée: 10 sept. 2001 → 13 sept. 2001

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	2142
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	15th International Workshop on Computer Science Logic, CSL 2001 and 10th Annual Conference of the European Association for Computer Science Logic, EACSL 2001
Pays/Territoire	France
La ville	Paris
période	10/09/01 → 13/09/01

Accès au document

10.1007/3-540-44802-0_5

Contient cette citation

Guglielmi, A., & Straßburger, L. (2001). Non-commutativity and MELL in the calculus of structures. Dans L. Fribourg (Ed.), Computer Science Logic: 15th International Workshop, CSL 2001 and 10th Annual Conference of the EACSL, Proceedings (p. 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. Editeur / 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)).

@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. Dans 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, p. 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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. Dans Fribourg L, Editeur, 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

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation