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

R. Maieli, Q. Puite

Research output: Contribution to journalArticleAcademicpeer-review

4 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


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

Cite this