Modularity of proof-nets : generating the type of a module

R. Maieli, Q. Puite

    Research output: Contribution to journalArticleAcademicpeer-review

    3 Citations (Scopus)
    1 Downloads (Pure)


    When we cut a multiplicative proof-net of linear logic in two parts we get two modules with a certain border. We call pretype of a module the set of partitions over its border induced by Danos-Regnier switchings. The type of a module is then defined as the double orthogonal of its pretype. This is an optimal notion describing the behaviour of a module: two modules behave in the same way precisely if they have the same type. In this paper we define a procedure which allows to characterize (and calculate) the type of a module only exploiting its intrinsic geometrical properties and without any explicit mention to the notion of orthogonality. This procedure is simply based on elementary graph rewriting steps, corresponding to the associativity, commutativity and weak-distributivity of the multiplicative connectives of linear logic.
    Original languageEnglish
    Pages (from-to)167-193
    JournalArchive for Mathematical Logic
    Issue number2
    Publication statusPublished - 2005

    Fingerprint Dive into the research topics of 'Modularity of proof-nets : generating the type of a module'. Together they form a unique fingerprint.

    Cite this