I am a Senior 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:* 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.

- 2020-11-23:
Slides and Video for “Resource Constrained Programming with Full Dependent Types” - 2020-08-13:
Quantitative Typing with Non-idempotent Intersection Types - 2020-01-24:
Slides for “Resource Constrained Programming with Full Dependent Types” - 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.

- Data types with Negation (Talk Abstract),
*MSFP 2022 (Talk Abstract)* - A Framework for Substructural Type Systems,
*ESOP 2022* - Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers,
*Under submission 2022* - A type- and scope-safe universe of syntaxes with binding: their semantics and proofs,
*Journal of Functional Programming 2021* - A Linear Algebra Approach to Linear Metatheory,
*Linearity-TLLA 2020* - Effect Handlers via Generalised Continuations,
*Journal of Functional Programming, 2020* - Dijkstra Monads for All,
*ICFP 2019* - A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs,
*ICFP 2018* - Context Constrained Computation,
*TyDe 2018 (Extended Abstract)* - The Syntax and Semantics of Quantitative Type Theory,
*LICS 2018* - Observed Communication Semantics for Classical Processes,
*ESOP 2017* - Compiling Parallel Functional Code with Data Parallel Idealised Algol,
*ArXiv (2017)* - Continuation Passing Style for Effect Handlers,
*FSCD 2017* - 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*