Computational Logic Publications, St Andrews University

The following is a list of recent or forthcoming reports and publications by the Computational Logic Group at the St Andrews University School of Computer Science. In each section, the most recent items are at the top. For publications by Juliana Bowles, Ian Gent or James McKinna, see their own web pages.

The links are mainly links to Postscript files. The files are usually not compressed. Sometimes there is a dvi file or a pdf file.

Accepted or published journal papers are copyright of the publisher: RD may be able to send a preprint or offprint.

Journal papers published or accepted

• R. Dyckhoff & S. Lengrand, Call-by-value lambda calculus and LJQ, Journal of Logic and Computation 17: pp 1109-1134, 2007. Abstract, PDF

• R. Dyckhoff & S. Negri, Decision methods for linearly ordered Heyting algebras, Archive for Mathematical Logic 45(4), pp 411-422, 2006. Abstract. ISSN: 0933-5846 (print version), ISSN: 1432-0665 (electronic version)

• R. Dyckhoff & C. Urban, Strong normalization of Herbelin's explicit substitution calculi with substitution propagation, Journal of Logic & Computation 13(5), pp 689--706, October 2003. Abstract, dvi, pdf, ps. (ISSN: 0955-792X)

• R. Dyckhoff & S. Negri, Admissibility of structural rules for extensions of contraction-free sequent calculi, Logic Journal of the IGPL 9, pp 573--580, 2001, Abstract, dvi, pdf, ps. (Print ISSN: 1367-0751 Online ISSN: 1368-9894)

• R. Dyckhoff & S. Negri, Admissibility of structural rules for contraction-free systems of intuitionistic logic, J. Symb. Logic 65, (December 2000), pp 1499--1518, Abstract, dvi, pdf, ps. (ISSN 0022-4812)

• A. A. Adams, A formalisation of weak normalisation (with respect to permutations) of sequent calculus proofs, LMS Journal of Computation and Mathematics 3, pp 1--26, 2000. Abstract, pdf.

• J. Caldwell, I. Gent & J. Underwood, Search Algorithms in Type Theory, Theoretical Computer Science 232, pp 55--90, 2000.

• R. Dyckhoff, A Deterministic Terminating Sequent Calculus for Gödel-Dummett logic, Logic Journal of the IGPL 7, pp 319--326, 1999. Abstract, dvi, ps. (Print ISSN: 1367-0751 Online ISSN: 1368-9894)

• R. Dyckhoff & L. Pinto, Permutability of proofs in intuitionistic sequent calculi, Theoretical Computer Science 212, pp 141--155, 1999. Abstract, dvi, ps Fuller version here.

• L. Pinto & R. Dyckhoff, Sequent calculi for the normal terms of the Lambda-Pi and Lambda-Pi-Sigma calculi , June 1998, (Proceedings of the CADE15-Workshop on Proof Search in Type Theoretic Languages), Electronic Notes in Theoretical Computer Science 17, 1998, 13 pp, ps.

• R. Dyckhoff & L. Pinto, Cut-elimination and a permutation-free sequent calculus for intuitionistic logic, Studia Logica 60, pp 107--118, 1998. pdf.

• R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, J. Symb. Logic 57, pp 795--807, 1992. (ISSN 0022-4812)

Refereed conference and workshop papers published or accepted

• S. Lengrand, R.Dyckhoff, J.McKinna, A Sequent Calculus for Type Theory, CSL 2006, (Proceedings), Lecture Notes in Computer Science 4207, pp 441--455, Springer Verlag, PDF.

• R. Dyckhoff, D. Kesner, S. Lengrand, Strong cut-elimination systems for Hudelmaier's depth-bounded sequent calculus for implicational logic, IJCAR 2006, (Proceedings, edited by U. Furbach and N. Shankar), Lecture Notes in Artificial Intelligence 4130, pp 347--361, Springer Verlag, PDF.

• R. Dyckhoff, S. Lengrand, LJQ: a strongly focused calculus for intuitionistic logic, Computability in Europe 2006, (Proceedings, edited by A. Beckmann et al), LNCS vol 3988, pp 173--185, Springer Verlag, PDF.

• K. Hammond, R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, S. Jost, H.-W. Loidl, G. Michaelson, R. Pointon, N. Scaife, J. érot, A. Wallace, Towards Formally Verifiable Resource Bounds for Real-Time Embedded Systems , Innovative Techniques for Certification of Embedded Systems, (Workshop Proceedings), PDF, 2006, 14pp.

• K. Hammond, R. Dyckhoff, C. Ferdinand, R. Heckmann, M. Hofmann, S. Jost, H.-W. Loidl, G. Michaelson, R. Pointon, N. Scaife, J. Sérot, A. Wallace, Towards Formally Verifiable WCET Analysis for a Functional Programming Language, WCET 06, (Workshop Proceedings), PDF, 2006, pp 56--61.

• K. Hammond, R. Dyckhoff, R. Heckmann, M. Hofmann, H.-W. Loidl, G. Michaelson, J. Sérot & A.Wallace, The EmBounded project (project paper), 6th Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, September 23--24 2005, pdf.

• R. Macinnis, J. McKinna, J. Parsons & R.Dyckhoff, A mechanised environment for Frege's Begriffsschrift notation, Workshop on Mathematical User Interfaces 2004, Bialowieza (Poland), September 18 2004, pdf.

• R. Dyckhoff & C.Urban, Strong normalization of Herbelin's explicit substitution calculi with substitution propagation, (revised version), Proceedings of the Fourth Workshop on Explicit Substitutions Theory and Applications (WESTAPP 01), Utrecht, May 20, 2001, (Pierre Lescanne, editor; Logic Group Preprint series No 210, Institute of Philosophy, University of Utrecht, ISBN 90-393-2764-5), pp 26-45, ps, pdf.

• R. Dyckhoff & L. Pinto, Proof search in constructive logics, Proceedings of Logic Colloquium 97, i.e. Sets and Proofs, edited by S.Barry Cooper & John K. Truss, pp 53--65, CUP, 1999, ps.

• C. Urban, Implementation of Proof Search in the Imperative Programming Language Pizza, In Proceedings of Tableaux '98, (Springer LNAI 1397), pp 313--319, 1998. ps.gz.
  

• J. Howe, Two loop-detection mechanisms: a comparison, In Proceedings of Tableaux '97 (Springer LNAI 1227), pp 188--200, 1997. ps.

• L. Pinto & R. Dyckhoff, Loop-free construction of counter-models for intuitionistic propositional logic and Correction, in: Symposia Gaussiana, Conf. A, Eds.: Behara/Fritsch/Lintz, Walter de Gruyter & Co, Berlin, New York, 1995, pp 225--232.. ps.

• L. Pinto & R. Dyckhoff, A constructive type system to integrate logic and functional programming, in: Proof search in type-theoretic languages (eds D. Galmiche & L. Wallen), Workshop 1B at 12th International Conference on Automated Deduction, Nancy, France, 1994, pp 70--81. ps.

• R. Dyckhoff & L. Pinto, Uniform proofs and natural deductions, in: Proof search in type-theoretic languages (eds D. Galmiche & L. Wallen), Workshop 1B at 12th International Conference on Automated Deduction, Nancy, France, 1994, pp 17--23. ps.

• L. Pinto, Cut formulae and logic programming, in: Extensions of Logic Programming (ed. R. Dyckhoff), Lect. Notes Art. Intell. 798, Springer-Verlag (1994), pp 282--300. ps.

• R. Dyckhoff, Implementing a simple proof assistant, in: Workshop on Programming for Logic Teaching (July 1987, ed. J. Derrick and H. A. Lewis), Centre for Theoretical Computer Science, University of Leeds, Proceedings 23.88, pp 49--59. pdf.

Research Reports (School of Computer Science, University of St Andrews)

• J. Kriener, M. Sadrzadeh & R. Dyckhoff, Implementation of a cut-free sequent calculus for logics with adjoint modalities, Research Report CS/09/01, 26 March 2009, 12 pp.
• S. Negri, Conservativity of apartness over equality, revisited, Research Report CS/99/4, 18 August 1999, 6 pp.
  
• J. Howe, A permutation-free sequent calculus for lax logic, Research Report CS/98/1, 3 April 1998, 30 pp.
  
• R. Dyckhoff, Dragalin's proofs of cut-admissibility for the intuitionistic sequent calculi G3i and G3i', Abstract, Research Report CS/97/8, August 1997, 20 pp. PDF
  
• R. Dyckhoff & L. Pinto, Permutability of proofs in intuitionistic sequent calculi (1.5MB), Research Report CS/97/7, June 1997, 30 pp. Brief version here.
  
• J. Howe, Theorem-proving and partial proof search for intuitionistic propositional logic using a permutation-free calculus with loop-checking, Research Report CS/96/12, December 1996, 28 pp.
  
• R. Dyckhoff & L. Pinto, A permutation-free sequent calculus for intuitionistic logic, Research Report CS/96/9, August 1996 (revised 17 September 1996), 28 pp.
  
• R. Dyckhoff & L. Pinto, Implementation of a loop-free method for construction of counter-models for intuitionistic propositional logic, Research Report CS/96/8, Revised February 2001, 17 pp, ps, pdf.
  
• A. A. Adams, Meta-theory in the Higher-Order Logic Framework Isabelle, Research Report CS/96/5, January 1996, 8 pp.
  
• R. Dyckhoff, Category theory as an extension of Martin-Löf type theory, Research Report CS/85/3, Revised in 1988, 16 pp.
  

Abstracts of conference submissions

• R. Dyckhoff, Contraction-free sequent calculi for Gödel-Dummett logic, abstract for LMPS 99 18 February, 1999, 2 pp.
  
• R. Dyckhoff, A deterministic terminating sequent calculus for propositional Dummett logic, abstract for Logic Colloquium 98, 15 April, 1998, 1 pp.
  

Theses

• S. Lengrand, Normalisation & Equivalence in Proof Theory & Type Theory, PhD thesis, St Andrews University and University of Paris 7, December 2006. (web page).
  
• R. Hardy, Formal methods for control engineering: a validated decision procedure for Nichols plot analysis, PhD thesis, St Andrews University, February 2006. (web page).
  
• J. M. Howe, Proof Search Issues in Some Non-Classical Logics, PhD thesis, St Andrews University, December 1998.
  
• A. Adams, Tools and techniques for machine-assisted meta-theory, PhD thesis, St Andrews University, November 1997
  
• C. Urban, Forum and its Implementation (MPhil thesis) St Andrews University, March 1997, 1p. (Full thesis available from Urban.) Abstract
  
• L. F. Pinto, Proof-theoretic investigations into integrated logical and functional programming, PhD thesis, St Andrews University, August 1996, 1p. (Full thesis available from Pinto.) Abstract.
  
• N. Leslie, Implementation of a Unification Algorithm in Martin-Löf Type Theory, MSc thesis, St Andrews University, 1993.
  
• T. Peillon, A proof editor for linear logic, MSc thesis, St Andrews University, 1992.
  
• M.Thomas, The imperative implementation of abstract data types, PhD thesis, St Andrews University, 1988.
  
• T. T. A. Hamza, Normalisation techniques in category theory and proof theory --- an implementation and applications, PhD thesis, St Andrews University, 1986.
  

Conference/workshop editions

• R. Dyckhoff, editor: Automated Reasoning with Analytic Tableaux and Related Methods, Springer Lect. Notes Art. Intell. 1847, (2000), 450 pp. Front Cover, Contents (Buy one at Amazon)
  
• R. Dyckhoff, editor: Automated Reasoning with Analytic Tableaux and Related Methods, Position Papers and Tutorials, Research Report CS/00/01, St Andrews University, 137 pp. Contents (Mail rd@dcs.st-and.ac.uk if you want a copy.)
  
• R. Dyckhoff, H. Herre and P. Schroeder-Heister, editors: Extensions of Logic Programming, Springer Lect. Notes Art. Intell. 1050, (1996), 318 pp. Contents (Mail rd@dcs.st-and.ac.uk if you want a copy; or try Amazon.)
  
• R. Dyckhoff, editor: Extensions of Logic Programming, Springer Lect. Notes Art. Intell. 798, (1994), 360 pp. (Buy one at Amazon.)

Book reviews

• R. Dyckhoff, Review of Computational Logic, by Ulrich Berger & Helmut Schwichtenberg, Nato 1998; (in the Journal of Functional Programming, 11 (4), 2001, pp 433-434).
  
• R. Dyckhoff, Review of Basic Proof Theory (2nd edition), by Anne Troelstra & Helmut Schwichtenberg, CUP, 2000; (in the Bulletin of Symbolic Logic 7 (2), 2001, p 280).
  
• R. Dyckhoff, Review of Practical Foundations of Mathematics, by Paul Taylor, CUP, 1999. (Also dvi).(in the Bulletin of the London Mathematical Society 32 (5), 2000, pp 619-622).
  
• R. Dyckhoff, Review of Basic Proof Theory (1st edition), , by Anne Troelstra & Helmut Schwichtenberg, CUP 1996; (in the Journal of Symbolic Logic 63, (1998), pp 1605-1606).
  
• R. Dyckhoff, Review of Semantics of Type Theory, by Thomas Streicher, Birkhauser Boston 1991, (in Formal Aspects of Computing 5, (1992) pp, pp 282-283).
  
• R. Dyckhoff, Review of Projection Factorisations in Partial Evaluation, by John Launchbury, CUP 1991; (in the Computer Journal 35 (1992), page 539).
  
• R. Dyckhoff, Review of Topos Theory, by Peter Johnstone, Academic Press 1977; (in Proc. Edinburgh Mathematical Society (1977)).
  
  

Other stuff

• A. Adams, SEQUEL Frameworks for the Theory of Sequent Calculus and Natural Deduction Systems (47KB), Internal report, Computer Science Division, St Andrews University, 1995.
  
• A. A. Adams, ALF as a Tool for Proving Properties of Sequent Calculus Systems (74KB), Internal report, Computer Science Division, St Andrews University, 1995.
• R. Dyckhoff, Factorisation theorems and projective spaces in topology, Mathematische Zeitschrift 127, 1972, Full text via DOI