Non-commutativity and MELL in the Calculus of Structures
Guglielmi, A. and Strassburger, L., 2001. Non-commutativity and MELL in the Calculus of Structures. In: Computer Science Logic (CSL) 2001 - Lecture Notes in Computer Science, 2001-09-01.
Related documents:This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.
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.
|Item Type||Conference or Workshop Items (Paper)|
|Creators||Guglielmi, A.and Strassburger, L.|
|Departments||Faculty of Science > Computer Science|
Actions (login required)