Older logic

  1. D.J. Pym. Editorial, Journal of Logic and Computation, Special Issue on Semantic Foundations of Proof-search. Journal of Logic and Computation 13(5):633–638, 2003.

  2. D.J. Pym Semantic Foundations of Proof-search, Special Issue of the Journal of Logic and Computation, 2004. Editor.

  3. D.J. Pym, P.W. O’Hearn, and H. Yang. Possible worlds and resources: the semantics of BI. Theoretical Computer Science 315(1): 257-305. Erratum: p. 285, l. -12: ‘, for some P′,Q ≡ P; P ’ should be ‘P ⊢ Q’.

  4. J.A, Harland and D. J. Pym. Resource-distribution via Boolean constraints. ACM Transactions on Computational Logic 4(1), 2003, 56–90.

  5. S.S. Ishtiaq and D. J. Pym. Kripke resource models of a dependently-typed, bunched λ-calculus. Journal of Logic and Computation 12(6):1061–1104, 2002.

  6. Didier Galmiche, Daniel Méry, and David Pym. Resource Tableaux (extended abstract). In Proc. CSL 2002, Edinburgh. LNCS 2471:183–199, 2002.

  7. Pablo Armelín and David Pym. Bunched Logic Programming (Extended Abstract). Proc. IJCAR 2001, LNAI 2083:289–304, 2001

  8. Corrections and Remarks. Research Report RR-00-04, Department of Computer Science, Queen Mary and Westfield College, University of London, 2000. ISSN 1470-5599.

  9. D.J. Pym. Notes Towards a Semantics for Proof-search. ENTCS 37 (2001). 18 pages.

  10. J.A. Harland, D.J. Pym, and M. Winikoff. Forward and Backward Chaining in Linear Logic. ENTCS 37 (2001). 16 pages.

  11. S.S. Ishtiaq and D. J. Pym. Kripke resource models of a dependently-typed, bunched λ-calculus (extended abstract). Proc. CSL 99. LNCS 1683:235–249, 1999.

  12. E. Ritter and D.J. Pym. On the semantics of classical disjunction. Journal of Pure and Applied Algebra 159 (2001) 315–338.

  13. D.J. Pym, E. Ritter, and L.A. Wallen. Proof-terms for classical and intuitionistic resolution. Journal of Logic and Computation 10(2) 173–207 2000.

  14. D.J. Pym. On Bunched Predicate Logic. Proc, LICS, 1999, IEEE Computer Society Press, 183–192.

  15. D.J. Pym and P.W. O’Hearn. The Logic of Bunched Implications. Bulletin of Symbolic Logic 5(2) 215–243 June 1999.

  16. D.J. Pym, E. ritter, and L.A. Wallen. On the intuitionistic force of classical search. Theoretical Computer Science 232 (2000) 299–333.

  17. S.S. Ishtiaq and D.J. Pym. A relevant analysis of natural deduction. Journal of Logic and Computation 8(6):809-838, 1998.

  18. P. Armelín and D. Pym. Logic Programming with Bunched Implications. ENTCS 17 (1998) 24pp.

  19. D. Galmiche and D. Pym. Proof-search in Type-theoretic Languages. Theoretical Computer Science 232 (2000) 5-53. (Joint work with D. Galmiche, INRIA-Nancy, France.)

  20. D. Galmiche and D. Pym (editors). Special Issue of Theoretical Computer Science, Proof-search in Type-theoretic Languages. TCS 232 (2000).

  21. J.A. Harland and D.J.Pym. Resource-distribution via Boolean constraints (extended abstract). Proc. CADE-14, W, McCune and G. Sutcliffe (editors), LNCS 1249:222–236, 1997.

  22. D.J. Pym. A note on representation and semantics in logical frameworks. Proc. CADE-13 Workshop, Proof-search in type-theoretic languages, D. Galmiche, ed., 1996.

  23. David Pym, Eike Ritter, and Lincoln Wallen. Proof-terms for classical and intuitionistic resolution (extended abstract). Proc. CADE-13, MacRobbie and Slaney, eds., LNCS, Springer, 1996.

  24. David Pym, Eike Ritter, and Lincoln Wallen. On the intuitionistic force of classical search (extended abstract). Proc. Tableaux 96, P. Miglioli, U. Moscato, D. Mundici, M. Orgnaghi, eds.. LNCS 1071: 295–311, Springer, 1996.

  25. J.A. Harland, D.J. Pym, and M. Winikoff. Programming in Lygon: a system demonstration. Proc. AMAST 96, M. Wirsing and M. Nivat, eds., LNCS 1101, 599, Springer, 1996.

  26. J.A. Harland, D.J. Pym, and M. Winikoff. Programming in Lygon: an overview. Proc. AMAST 96, M. Wirsing and M. Nivat, eds.. LNCS 1101:391–405, Springer, 1996.

  27. D. Murphy, L. Pryor, and D. Pym. A note on processes for plan-execution an powerdomains for plan-comparison. QMWC Technical Report, 1996.

  28. D.J. Pym. Functorial Kripke Models of the λΠ-calculus. (Given as an Invited Lecture, EU Workshop on Proof Theory and Computation, Leeds University, September, 1994; and as an Invited Lecture, Newton Institute (Cambridge), Semantics of Computation Programme, Workshop on Category Theory and Logic Programming, September, 1995.)

  29. D.J. Pym. What is a linear logic programming language? (Given as an Invited Lecture, Newton Institute (Cambridge), Semantics of Computation Programme, Workshop on Linear Logic, November, 1995.

  30. J.A. Harland, D.J. Pym, and M. Winikoff. Programming in Lygon: A Brief Overview. Proc. ILPS 95, J. Lloyd (editor), 636, MIT Press, 1995. Also available as Technical Report 708, Department of Computer Science, Queen Mary and Westfield College, University of London.

  31. D. Murphy, L. Pryor, and D. Pym. Actions as processes: a position on planning. Working Notes of the AAAI Spring Symposium on Extending Theories of Action: Formal Theory and Practical Applications, Stanford University, 1995, 169–173.

  32. J.A, Harland and D. J. Pym. A Note on the Implementation and Applications of Linear Logic Programming Languages. Annual Computer Science Communications 16(1), 1994, 647-658.

  33. D.J. Pym. A Note on the Proof Theory [of] the λΠ-calculus. Studia Logica 54(2), 1995, 199-230. Preprint available as: Technical Report No. 694, Department of Computer Science, Queen Mary and Westfield College, University of London.

  34. J.A, Harland and D. J. Pym. A Uniform Proof-theoretic Investigation of Linear Logic Programming. Journal of Logic and Computation 4(2), 175–207, 1994.

  35. D.J. Pym. Errata and Remarks. University of Edinburgh Report ECS-LFCS-93-265, May 1993.

  36. J.A, Harland and D. J. Pym.A Synopsis on the Identification of Linear Logic Programming Languages. University of Edinburgh Report ECS-LFCS-92-248, November 1992.

  37. D.J. Pym and L.A. Wallen. Logic Programming via Proof-valued Computations. In: Proc. 4th UK Conference on Logic Programming, London, 1992, K. Broda (editor), Springer, 1992, 253-262. Also available as University of Edinburgh Report ECS-LFCS-92-246.

  38. D.J. Pym. A Unification Algorithm for the λΠ-calculus. Int. J. of Foundations of Computer Science, Vol. 3, No. 3, 333–378, 1992. Pre-publication version available as University of Edinburgh Report ECS-LFCS-92-229.

  39. J.A. Harland and D.J. Pym. On Resolution in Fragments of Classical Linear Logic. LNAI 624, 30–41, Springer-Verlag, 1992. Also available as University of Edinburgh LFCS Report ECS-LFCS-212, May 1992.

  40. J.A. Harland and D.J. Pym. The Uniform Proof-theoretic Foundation of Linear Logic Programming (Extended Abstract). In: Proc. International Symposium on Logic Programming, V. Saraswat and K. Ueda (editors), 304–318, MIT Press, 1991. Also available as University of Edinburgh LFCS Report ECS-LFCS-91-168.

  41. D.J. Pym and L.A. Wallen. Proof-search in the λΠ-calculus. In: Logical Frameworks, G.P. Huet and G.D. Plotkin (editors), Cambridge University Press, 1991, 309–340. Also available as University of Edinburgh LFCS Report ECS-LFCS-91-146, April 1991.

  42. D.J. Pym. Proofs, Search and Computation in General Logic. Ph.D. Thesis, University of Edinburgh, 1990. University of Edinburgh Report CST-69-90 (also ECS-LFCS-90-125), November 1990.

  43. J.A, Harland and D. J. Pym. The Uniform Proof-theoretic Foundation of Linear Logic Programming. University of Edinburgh LFCS Report ECS-LFCS-90-124, November 1990.

  44. D.J. Pym and L.A. Wallen. Investigations into Proof-search in a System of First-order Dependent Function Types. LNAI 449:236–250, 1990. Also available as ECS-LFCS-90-111, University of Edinburgh, March 1990.