A system of interaction and structure V: the exponentials and splitting


Guglielmi, A. and Straburger, L., 2011. A system of interaction and structure V: the exponentials and splitting. Mathematical Structures in Computer Science, 21 (3), pp. 563-584.

Related documents:

PDF (Guglielmi_MSCS_2011_21_3_563.pdf) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (2635kB) | Preview

    Official URL:

    Related URLs:


    System NEL is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials, or, equivalently, it is MELL augmented with the non-commutative self-dual connective seq. NEL is presented in deep inference, because no Gentzen formalism can express it in such a way that the cut rule is admissible. Other recent work shows that system NEL is Turing-complete, and is able to express process algebra sequential composition directly and model causal quantum evolution faithfully. In this paper, we show cut elimination for NEL, based on a technique that we call splitting. The splitting theorem shows how and to what extent we can recover a sequent-like structure in NEL proofs. When combined with a 'decomposition' theorem, proved in the previous paper of this series, splitting yields a cut-elimination procedure for NEL.


    Item Type Articles
    CreatorsGuglielmi, A.and Straburger, L.
    Related URLs
    URLURL Type
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementGuglielmi_MSCS_2011_21_3_563.pdf: © Cambridge University Press 2011
    ID Code24049


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...