•  17
    Pragmatic and dialogic interpretations of bi-intuitionism. Part II
    with Massimiliano Carrara, Daniele Chiffi, and Alessandro Menti
    Logic and Logical Philosophy. 2014.
  •  24
    Pragmatic and dialogic interpretations of bi-intuitionism. Part 1
    with Massimiliano Carrara, Daniele Chiffi, and Alessandro Menti
    Logic and Logical Philosophy 23 (4): 449-480. 2014.
    We consider a “polarized” version of bi-intuitionistic logic [5, 2, 6, 4] as a logic of assertions and hypotheses and show that it supports a “rich proof theory” and an interesting categorical interpretation, unlike the standard approach of C. Rauszer’s Heyting-Brouwer logic [28, 29], whose categorical models are all partial orders by Crolard’s theorem [8]. We show that P.A. Melliès notion of chirality [21, 22] appears as the right mathematical representation of the mirror symmetry between the i…Read more
  •  22
    Errata Corrige to “Pragmatic and dialogic interpretation of bi-intuitionism. Part I”
    with Massimiliano Carrara, Daniele Chiffi, and Alessandro Menti
    Logic and Logical Philosophy 25 (2). 2016.
  • Few systems for mechanical proof-checking have been used so far to transform formal proofs rather than to formalize informal arguments and to verify correctness. The unwinding of proofs, namely, the process of applying lemmata and extracting explicit values for the parameters within a proof, is an obvious candidate for mechanization. It corresponds to the procedures of Cut-elimination and functional interpretation in proof-theory and allows the extraction of the constructive content of a proof, …Read more
  • On the [Pi]-Calculus and Linear Logic
    with P. J. Scott
    LFCS, Department of Computer Science, University of Edinburgh. 1992.
  •  41
    Planar and braided proof-nets for multiplicative linear logic with mix
    with A. Fleury
    Archive for Mathematical Logic 37 (5-6): 309-325. 1998.
    We consider a class of graphs embedded in $R^2$ as noncommutative proof-nets with an explicit exchange rule. We give two characterization of such proof-nets, one representing proof-nets as CW-complexes in a two-dimensional disc, the other extending a characterization by Asperti. As a corollary, we obtain that the test of correctness in the case of planar graphs is linear in the size of the data. Braided proof-nets are proof-nets for multiplicative linear logic with Mix embedded in $R^3$ . In ord…Read more