The following is a list of ancient, recent or forthcoming reports and publications by Roy Dyckhoff and/or his students and collaborators at the St Andrews University School of Computer Science. For others in the Computational Logic Group, 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
S. 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, PDF
N. Francez & R. Dyckhoff, Proof-theoretic semantics for a natural language fragment, Linguistics & Philosophy 33, pp 447--477, 2010. Abstract, PDF
M. 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, PDF
M. 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, 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)
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)
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), pdf
R. Dyckhoff, Cut-elimination, substitution and normalisation, Dag Prawitz on Proofs and Meaning (ed. H Wansing) in "Outstanding Contributions to Logic" 7, pp 163--189, Springer, 2015.
R. Dyckhoff, S. Negri Coherentisation of accessibility conditions in labelled sequent calculi, (Extended Abstract) "Gentzen Systems and Beyond" Workshop, Vienna Summer of Logic, 2pp, 13 July 2014, 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.
Implementation of Proof Search
in the Imperative Programming Language Pizza, In Proceedings
of Tableaux '98, (Springer LNAI
1397), pp 313--319, 1998. ps.gz.
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.