Computer Science @ University of St Andrews

University of St Andrews crest

CS Person

Dr Roy Dyckhoff

Position: Honorary Senior Lecturer

Email ( rd

Home page:

Research Overview

intuitionistic logic; constructive logic; constructive mathematics; automated reasoning; category theory; logic programming; proof theory; type theory; functional programming; lambda calculus; programming language semantics; computational linguistics

Recent Publications

Indefinite proof and inversions of syllogisms

Contraction-free sequent calculi in intuitionistic logic: a correction

Analyticity, balance and non-admissibility of Cut in Stoic Logic

Commentary on Grigori Mints’ “Classical and Intuitionistic Geometric Logic”

Intuitionistic decision procedures since Gentzen

Dyckhoff, R 2016, Intuitionistic decision procedures since Gentzen. in R Kahle, T Strahm & T Studer (eds), Advances in Proof Theory. Progress in Computer Science and Applied Logic, vol. 28, Birkhäuser Basel, pp. 245-267, apt13 Advances in Proof Theory, Bern, Switzerland, 13/12/13. DOI: 10.1007/978-3-319-29198-7_6

POSIX lexing with derivatives of regular expressions (proof pearl)

Ausaf, F, Dyckhoff, R & Urban, C 2016, POSIX lexing with derivatives of regular expressions (proof pearl). in JC Blanchette & S Merz (eds), Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9807, Springer, pp. 69-86, ITP 2016: Interactive Theorem Proving, Nancy, France, 22/08/16. DOI: 10.1007/978-3-319-43144-4_5

Some remarks on proof-theoretic semantics

Dyckhoff, R 2016, Some remarks on proof-theoretic semantics. in T Piecha & P Schroeder-Heister (eds), Advances in Proof-Theoretic Semantics. Trends in Logic, vol. 43, Springer, pp. 79-93, Second Conference on Proof-Theoretic Semantics, Tübingen, Germany, 8/03/13. DOI: 10.1007/978-3-319-22686-6_5

Geometrisation of first-order logic

Cut-elimination, substitution and normalisation

Dyckhoff, R 2015, Cut-elimination, substitution and normalisation. in H Wansing (ed.), Dag Prawitz on Proofs and Meaning. Outstanding Contributions to Logic, vol. 7, Springer, pp. 163-187. DOI: 10.1007/978-3-319-11041-7_7

Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators