Dr Robert Atkey

Senior Lecturer

Computer and Information Sciences


Personal statement

I am a Chancellor’s Fellow and Lecturer in the department of Computer and Information Sciences at the University of Strathclyde. I am a member the department’s Mathematically Structured Programming (MSP) group.

My research is on the design and analysis of programming languages. I use mathematical ideas and structure from logic, category theory, type theory, and denotational semantics to study programming languages and the systems they describe. I was co-chair of the 2016 workshop on Mathematically Structured Functional Programming, and served on the programme committee for POPL 2016. I am on the programme committee for the upcoming ESOP 2017.

I have done and am doing research in the following areas of programming languages:

The Theory of Parametricity is the analysis of programming languages in terms of how they operate under notions of “change”. Classically, this is the study of programs' behaviour under change of data representation. I have extended the original concept to study higher-kinded type systems (as one finds in languages like Scala or Haskell) and dependent type systems. I have also worked on mechanised models of parametricity in the Coq theorem prover.

I have Applied Parametricity to representation of syntax, representations of domain-specfic languages (DSLs), invariance properties in geometry and classical mechanics, and developed its application to dimension-correct scientific programming. I am currently exploring the connections between classical parametricity and systems that study how programs change behaviour under change of input. I am also interested in using parametricity to study the ideal-world/real-world distinction in cryptography. I gave an invited talk at the Off the Beaten Track workshop on how I see this interesting research field developing.

I have built Resource-aware Verifiers and Type Systems. I have worked on program logics and automated verification of resource usage, and on type systems for tracking resource usage in type systems, in terms of resource relationships and communication.

In effects and effect systems, I studied Parameterised monads, which have become a popular way to track the effects in programs, going beyond monads. I developed the theory of parameterised monads to algebraic presentations, with application to effect-driven program optimisations. I have also worked on reasoning about recursive data types in the presence of effects. There is a blog post describing this work, and papers about the fibration-theory foundations, and reasoning techniques for Haskell programming.

From 2013 to 2014 I developed Static Analysis Tools for Java Concurrency at Contemplate. We built ThreadSafe, a tool to discover and analyse concurrency defects in Java programs. I wrote some developer-oriented articles on using ThreadSafe to discover race conditions and deadlocks. With Don Sannella, I wrote an academic paper discussing ThreadSafe's internals and our experiences in applying academic static analysis ideas to industry. My work at Contemplate was informed by my academic research on mechanised models of the JVM, proof-carrying code, and reseource consumption verification.

Back to staff profile


Polynomial time and dependent types
Atkey Robert
Proceedings of the ACM on Programming Languages (PACMPL) Vol 8, pp. 2288–2317 (2024)
Compiling higher-order specifications to SMT solvers : how to deal with rejection constructively
Daggitt Matthew L, Atkey Robert, Kokke Wen, Komendantskaya Ekaterina, Arnaboldi Luca
CPP 2023 : Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs , pp. 102-120 (2023)
A framework for substructural type systems
Wood James, Atkey Robert
ESOP 2022 Proceedings European Symposium on Programming 2022 Lecture Notes in Computer Science (2022)
A linear algebra approach to linear metatheory
Wood James, Atkey Robert
Linearity & Trends in Linear Logic and its Application 2020, pp. 195-212 (2021)
A type and scope safe universe of syntaxes with binding : their semantics and proofs
Allais Guillaume, Atkey Robert, Chapman James, McBride Conor, McKinna James
Journal of Functional Programming Vol 31 (2021)
Neural networks, secure by construction : an exploration of refinement types
Kokke Wen, Komendantskaya Ekaterina, Kienitz Daniel, Atkey Bob, Aspinall David
The 18th Asian Symposium on Programming Languages and Systems (2020)

More publications

Back to staff profile

Professional Activities

External examiner for Craig McLaughlin's PhD thesis
Invited Talk “Resource Constrained Programming with Full Dependent Types”
Invited talk “Type Theory and Sympathy”
Jury member for Kenji Malliard's thesis defence
External Examiner for Frantisek Farka's PhD thesis
Scottish Programming Languages and Verification Summer School 2019

More professional activities


AISEC: AI Secure and Explainable by Construction
Atkey, Bob (Principal Investigator)
01-Jan-2020 - 09-Jan-2024
KTP - Cambridge Quantum Computing (CQC) / R190328-202
McBride, Conor (Principal Investigator) Atkey, Bob (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
24-Jan-2020 - 23-Jan-2022
KTP - Cambridge Quantum Computing (CQC)
McBride, Conor (Principal Investigator) Atkey, Bob (Co-investigator) Nordvall Forsberg, Fredrik (Co-investigator)
24-Jan-2020 - 23-Jan-2022
Industrial Case Account - University of Strathclyde 2019 | Fontana, Enrico
Kupke, Clemens (Principal Investigator) Atkey, Bob (Co-investigator) Fontana, Enrico (Research Co-investigator)
01-Jan-2019 - 01-Jan-2024
‘Social smart contracts’ for food safety
Terzis, Sotirios (Principal Investigator) Atkey, Bob (Co-investigator) Chapman, James (Co-investigator)
11-Jan-2017 - 29-Jan-2018
KTP - Symphonic Software
Atkey, Bob (Principal Investigator) Kupke, Clemens (Co-investigator)
06-Jan-2017 - 05-Jan-2019

More projects

Back to staff profile


Dr Robert Atkey
Senior Lecturer
Computer and Information Sciences

Email: robert.atkey@strath.ac.uk
Tel: 548 2954