8 found
Order:
See also
Jean-Baptiste Joinet
Jean Moulin Lyon 3 University
  1.  73
    A new deconstructive logic: Linear logic.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1997 - Journal of Symbolic Logic 62 (3):755-807.
    The main concern of this paper is the design of a noetherian and confluent normalization for LK 2. The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD, delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of `programming-with-proofs' to classical logic ; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic using (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  2.  28
    LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - In Jean-Yves Girard, Yves Lafont & Laurent Regnier (eds.), Advances in Linear Logic. Cambridge University Press. pp. 222--211.
  3. Ouro Preto (Minas Gerais), Brazil July 29–August 1, 2003.France Xii, Marcelo Coniglio, Gilles Dowek, Jouko Väänanen, Renata Wassermann, Eric Allender, Jean-Baptiste Joinet & Dale Miller - 2004 - Bulletin of Symbolic Logic 10 (2).
  4.  35
    On the linear decoration of intuitionistic derivations.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - Archive for Mathematical Logic 33 (6):387-412.
    We define an optimal proof-by-proof embedding of intuitionistic sequent calculus into linear logic and analyse the (purely logical) linearity information thus obtained.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  5.  35
    Completeness of MLL Proof-Nets w.r.t. Weak Distributivity.Jean-Baptiste Joinet - 2007 - Journal of Symbolic Logic 72 (1):159 - 170.
    We examine 'weak-distributivity' as a rewriting rule $??$ defined on multiplicative proof-structures (so, in particular, on multiplicative proof-nets: MLL). This rewriting does not preserve the type of proof-nets, but does nevertheless preserve their correctness. The specific contribution of this paper, is to give a direct proof of completeness for $??$: starting from a set of simple generators (proof-nets which are a n-ary ⊗ of &-ized axioms), any mono-conclusion MLL proof-net can be reached by $??$ rewriting (up to ⊗ and & (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  6.  29
    From abstraction and indiscernibility to classification and types.Jean-Baptiste Joinet & Thomas Seiller - 2021 - Kagaku Tetsugaku 53 (2):65-93.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  7.  21
    SN and {CR} for free-style {${bf LK}sp {tq}$}: linear decorations and simulation of normalization.Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora de Falco - 2002 - Journal of Symbolic Logic 67 (1):162-196.
    The present report is a, somewhat lengthy, addendum to "A new deconstructive logic: linear logic," where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.The main novelty here is the observation that this type-distinction is not essential: we can allow classical (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8.  15
    SN and CR for free-style LKtq: linear decorations and simulation of normalization.Jean-Baptiste Joinet, Harold Schellinx & Lorenzo Tortora De Falco - 2002 - Journal of Symbolic Logic 67 (1):162-196.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark