1.  7
    Peter W. O'Hearn & David J. Pym (1999). The Logic of Bunched Implications. 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 (7 more)  
    Export citation  
    My bibliography   4 citations  
  2.  13
    David J. Pym (2004). Reductive Logic and Proof-Search: Proof Theory, Semantics, and Control. 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  
    Export citation  
    My bibliography   1 citation  
  3.  51
    David J. Pym (1995). A Note on the Proof Theory the λII-Calculus. Studia Logica 54 (2):199 - 230.
    The II-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 II-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 here (...)
    Direct download (6 more)  
    Export citation  
    My bibliography