Bob Atkey

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.

Blog posts

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

Publications

See also DBLP or Google Scholar.

A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs, Under submission
Dijkstra Monads for All, ICFP 2019
Effect Handlers via Generalised Continuations, Under submission
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, Under submission
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