4 found
Order:
  1.  42
    The Structure of Multiplicatives.Vincent Danos & Laurent Regnier - 1989 - Archive for Mathematical Logic 28 (3):181-203.
    Investigating Girard's new propositionnal calculus which aims at a large scale study of computation, we stumble quickly on that question: What is a multiplicative connective? We give here a detailed answer together with our motivations and expectations.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   35 citations  
  2.  35
    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 (8 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  3.  11
    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.
  4.  29
    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 (4 more)  
     
    Export citation  
     
    Bookmark   1 citation