Order:
  1.  35
    The Logic of Bunched Implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
    We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic (...)
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   22 citations  
  2. Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control.David J. Pym & Eike Ritter - 2004 - Oxford, England: Oxford University Press.
    This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search, areas of logic that are becoming important in computer science. A systematic foundational text on these emerging topics, it includes proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences. Suitable for researchers and graduate students in mathematical, computational and philosophical logic, and in (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  3.  68
    A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
    The lambdaPi-calculus, a theory of first-order dependent function types in Curry-Howard-de Bruijn correspondence with a fragment of minimal first-order logic, is defined as a system of (linearized) natural deduction. In this paper, we present a Gentzen-style sequent calculus for the lambdaPi-calculus and prove the cut-elimination theorem. The cut-elimination result builds upon the existence of normal forms for the natural deduction system and can be considered to be analogous to a proof provided by Prawitz for first-order logic. The type-theoretic setting considered (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  4. A Synopsis on the Identification of Linear Logic Programming Languages.J. A. Harland & David J. Pym - 1992 - LFCS, Department of Computer Science, University of Edinburgh.
     
    Export citation  
     
    Bookmark  
  5. On Resolution in Fragments of Classical Linear Logic.J. A. Harland & David J. Pym - 1992 - LFCS, Department of Computer Science, University of Edinburgh.
     
    Export citation  
     
    Bookmark  
  6.  25
    Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control.David J. Pym - 2004 - Oxford, England: Oxford University Press.
    This book is a specialized monograph on the development of the mathematical and computational metatheory of reductive logic and proof-search including proof-theoretic, semantic/model-theoretic and algorithmic aspects. The scope ranges from the conceptual background to reductive logic, through its mathematical metatheory, to its modern applications in the computational sciences.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  7. Logic Programming Via Proof-Valued Computations.David J. Pym & Lincoln A. Wallen - 1992 - LFCS, Department of Computer Science, University of Edinburgh.
     
    Export citation  
     
    Bookmark   1 citation