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.

R. Dyckhoff, M. Sadrzadeh & J. Truffaut, Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators, ACM Transactions on Computational Logic, published online, 2013. DOI: 10.1145/2536740.2536742. Abstract, PDF

R. Dyckhoff & S. Negri, A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel-McKinsey-Tarski embedding, Journal of Logic and Computation, published online, 2013. DOI: 10.1093/logcom/ext036. Abstract, PDF

R. Dyckhoff & S. Negri, Proof analysis in intermediate logics, Archive for Mathematical Logic

**51**, pp 71--92, 2012. DOI: 10.1007/s00153-011-0254-7. Abstract, PDFN. Francez & R. Dyckhoff, A note on harmony, Journal of Philosophical Logic published online, 2011. DOI: 10.1007/s10992-011-9208-0 Also as Volume

**41**, pp 613--628, 2012. Abstract, PDFS. Lengrand, R. Dyckhoff & J. McKinna, A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems, Logical Methods in Computer Science

**7**(1:6), pp. 1--35, 2011. DOI: 10.2168/LMCS-7(1:6)2011. Abstract, PDFN. Francez & R. Dyckhoff, Proof-theoretic semantics for a natural language fragment, Linguistics & Philosophy

**33**, pp 447--477, 2010. Abstract, PDFM. Sadrzadeh & R. Dyckhoff, Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information (full version), Review of Symbolic Logic

**3**: pp 351--373, 2010. Abstract, PDFN. Francez, R. Dyckhoff & G. Ben Avi, Proof-Theoretic Semantics for Subsentential Phrases, Studia Logica

**94**: pp 381--401, 2010. Abstract, PDFM. Sadrzadeh & R. Dyckhoff, Positive Logic with Adjoint Modalities: Proof Theory, Semantics and Reasoning about Information (short version), Electronic Notes in Theoretical Computer Science

**249**: pp 451--470, 2009. Abstract, PDFR. Dyckhoff & S. Lengrand, Call-by-value lambda calculus and

**LJQ**, Journal of Logic and Computation**17**: pp 1109--1134, 2007. Abstract, PDFR. 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, pdf, 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)

N. Francez, R.Dyckhoff, Proof-Theoretic Semantics for a Natural Language Fragment, MOL 2007, (Proceedings), Lecture Notes in Computer Science 6149, pp 56--71, Springer Verlag, PDF.

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.

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

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

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

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

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

- 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