# 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

Dyckhoff, R & Negri, S 2015, 'Geometrisation of first-order logic'

*Bulletin of Symbolic Logic*, vol 21, no. 2, pp. 123–163. DOI: 10.1017/bsl.2015.7### 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

Dyckhoff, R, Sadrzadeh, M & Truffaut, J 2013, 'Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators'

*ACM Transactions on Computational Logic*, vol 14, no. 4, 34. DOI: 10.1145/2536740.2536742### A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–McKinsey–Tarski embedding

Dyckhoff, R & Negri, S 2013, 'A cut-free sequent system for Grzegorczyk logic, with an application to the Gödel–McKinsey–Tarski embedding'

*Journal of Logic and Computation*. DOI: 10.1093/logcom/ext036### A note on harmony

Dyckhoff, R & Francez, N 2012, 'A note on harmony'

*Journal of Philosophical Logic*, vol 41, no. 3, pp. 613–628.### Proof Analysis in Intermediate Logics

Dyckhoff, R & Negri, S 2012, 'Proof Analysis in Intermediate Logics'

*Archive for Mathematical Logic*, vol 51, no. 1-2, pp. 71–92. DOI: 10.1007/s00153-011-0254-7
Follow us: