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.

- 2016-10-10:
Off the Beaten Track 2017: Call for Talk Proposals - 2016-04-12:
Authenticated Data Structures, as a Library, for Free! - 2016-01-26:
Slides and notes for my OBT “Generalising Abstraction” talk - 2015-04-23:
The Incremental λ-Calculus and Relational Parametricity - 2015-04-19:
Slides for “An Algebraic Approach to Typechecking and Elaboration” - 2015-04-17:
Propositions as Filenames, Builds as Proofs: The Essence of Make - 2014-01-29:
POPL Slides - 2013-07-17:
One Done, Two Submitted - 2013-03-29:
Productive Coprogramming with Guarded Recursion - 2012-11-07:
Theorems for Free - 2012-11-07:
Abstraction and Invariance for Algebraically Indexed Types - 2012-09-06:
Interleaving Data and Effects - 2012-09-05:
Relational Parametricity for Higher Kinds - 2012-01-06:
Reasoning about Stream Processing with Effects - 2011-12-14:
A Type Checker that knows its Monad from its Elbow - 2011-11-14:
How to be a Productive Programmer - 2011-04-28:
On Structural Recursion II: Folds and Induction - 2011-04-22:
On Structural Recursion

See also DBLP or Google Scholar.

- A Scope Safe Universe of Syntaxes with Binding, Their Semantics and Proofs,
*Under submission* - Observed Communication Semantics for Classical Processes,
*ESOP 2017* - Compiling Parallel Functional Code with Data Parallel Idealised Algol,
*Under submission* - Continuation Passing Style for Effect Handlers,
*Under submission* - Conflation Confers Concurrency,
*WadlerFest 2016* - Models for Polymorphism over Physical Dimensions,
*TLCA 2015* - Interleaving data and effects,
*Journal of Functional Programming, 2015* - ThreadSafe: Static Analysis for Java Concurrency,
*AVoCS 2015* - From Parametricity to Conservation Laws, via Noether's Theorem,
*POPL 2014* - A Relationally Parametric Model of Dependent Type Theory,
*POPL 2014* - Abstraction and Invariance for Algebraically Indexed Types,
*POPL 2013* - Productive Coprogramming with Guarded Recursion,
*ICFP 2013* - Relational Parametricity for Higher Kinds,
*CSL 2012* - Fibrational Induction Meets Effects,
*FoSSaCS 2012* - Refining Inductive Types,
*Logical Methods in Computer Science, 2012* - The Semantics of Parsing with Semantic Actions,
*LICS 2012* - Amortised Resource Analysis with Separation Logic,
*Logical Methods in Computer Science, 2011* - When Is a Type Refinement an Inductive Type?,
*FoSSaCS 2011* - Amortised Resource Analysis with Separation Logic,
*ESOP 2010* - Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode,
*TGC 2010* - Algebras for Parameterised Monads,
*CALCO 2009* - A Deep Embedding of Parametric Polymorphism in Coq,
*WMM 2009* - Parameterised notions of computation,
*Journal of Functional Programming, 2009* - Syntax for Free: Representing Syntax with Binding Using Parametricity,
*TLCA 2009* - Unembedding domain-specific languages,
*Haskell Symposium 2009* - What is a Categorical Model of Arrows?,
*MSFP 2008* - Secure Execution of Mobile Java using Static Analysis and Proof Carrying Code,
*UK e-Science AHM 2007* - CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types,
*TYPES 2007* - Specifying and Verifying Heap Space Allocation with JML and ESC/Java2,
*FTfJP 2006* - Parameterised Notions of Computation,
*MSFP 2006* - Substructural Simple Type Theories for Separation and In-place Update,
*PhD Thesis* - A 𝜆-Calculus for Resource Separation,
*ICALP 2004*