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 of the department’s Mathematically Structured Programming (MSP) group.
Email: bob.atkey@gmail.com or robert.atkey@strath.ac.uk
My research is on 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.
The Theory of Parametricity is the analysis of programming languages in terms of how they operate under “change” of inputs or representation. I have extended the original concept to study higher-kinded types (as one finds in Scala and Haskell) and dependent types. 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-specific languages (DSLs), invariance properties in geometry and classical mechanics, and 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 in the presence of effects.
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 resource consumption verification in Java.
See also DBLP or Google Scholar.