Proof nets for additive linear logic with units


Heijltjes, W., 2011. Proof nets for additive linear logic with units. In: 2011 26th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, pp. 207-216.

Related documents:

PDF (Author's accepted version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
Download (188kB) | Preview

    Official URL:


    Additive linear logic, the fragment of linear logic concerning linear implication between strictly additive formu- lae, coincides with sum-product logic, the internal language of categories with free finite products and coproducts. Deciding equality of its proof terms, as imposed by the categorical laws, is complicated by the presence of the units (the initial and terminal objects of the category) and the fact that in a free setting products and coproducts do not distribute. The best known desicion algorithm, due to Cockett and Santocanale (CSL 2009), is highly involved, requiring an intricate case analysis on the syntax of terms. This paper provides canonical, graphical representations of the categorical morphisms, yielding a novel solution to this decision problem. Starting with (a modification of) existing proof nets, due to Hughes and Van Glabbeek, for additive linear logic without units, canonical forms are obtained by graph rewriting. The rewriting algorithm is remarkably simple. As a decision procedure for term equality it matches the known complexity of the problem. A main technical contribution of the paper is the substantial correctness proof of the algorithm.


    Item Type Book Sections
    CreatorsHeijltjes, W.
    DepartmentsFaculty of Science > Computer Science
    Publisher StatementSigma_Pi.pdf: © 2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
    ID Code32342
    Additional InformationISSN 1043-6871


    Actions (login required)

    View Item

    Document Downloads

    More statistics for this item...