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.D.J. Pym Semantic Foundations of Proof-search, Special Issue of the Journal of Logic and Computation, 2004. Editor.

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*’.J.A, Harland and D. J. Pym. Resource-distribution via Boolean constraints.

*ACM Transactions on Computational Logic*4(1), 2003, 56–90.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.Didier Galmiche, Daniel Méry, and David Pym. Resource Tableaux (extended abstract). In

*Proc. CSL 2002*, Edinburgh. LNCS 2471:183–199, 2002.Pablo Armelín and David Pym. Bunched Logic Programming (Extended Abstract).

*Proc. IJCAR 2001*, LNAI 2083:289–304, 2001Corrections and Remarks. Research Report RR-00-04, Department of Computer Science, Queen Mary and Westfield College, University of London, 2000. ISSN 1470-5599.

D.J. Pym. Notes Towards a Semantics for Proof-search.

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

*ENTCS*37 (2001). 16 pages.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.E. Ritter and D.J. Pym. On the semantics of classical disjunction.

*Journal of Pure and Applied Algebra*159 (2001) 315–338.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.D.J. Pym. On Bunched Predicate Logic.

*Proc, LICS*, 1999, IEEE Computer Society Press, 183–192.D.J. Pym and P.W. O’Hearn. The Logic of Bunched Implications.

*Bulletin of Symbolic Logic*5(2) 215–243 June 1999.D.J. Pym, E. ritter, and L.A. Wallen. On the intuitionistic force of classical search.

*Theoretical Computer Science*232 (2000) 299–333.S.S. Ishtiaq and D.J. Pym. A relevant analysis of natural deduction.

*Journal of Logic and Computation*8(6):809-838, 1998.P. Armelín and D. Pym. Logic Programming with Bunched Implications.

*ENTCS*17 (1998) 24pp.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.)D. Galmiche and D. Pym (editors). Special Issue of

*Theoretical Computer Science*, Proof-search in Type-theoretic Languages. TCS 232 (2000).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.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.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.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.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.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.D. Murphy, L. Pryor, and D. Pym. A note on processes for plan-execution an powerdomains for plan-comparison. QMWC Technical Report, 1996.

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.)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.

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.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.

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.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.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.D.J. Pym. Errata and Remarks. University of Edinburgh Report ECS-LFCS-93-265, May 1993.

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.

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.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.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.

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.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.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.

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.

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.