Computer Science @ University of St Andrews

University of St Andrews crest

Dr Roy Dyckhoff

Dr Roy Dyckhoff

Position: Honorary Senior Lecturer

Email (@st-andrews.ac.uk): roy.dyckhoff

Home page: https://rd.host.cs.st-andrews.ac.uk

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

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-14 December. 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-27 August. 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-10 March. 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

A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–McKinsey–Tarski embedding

A note on harmony

Proof Analysis in Intermediate Logics

Proof-theoretic semantics for a natural language fragment