Bob Atkey

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.

Blog posts

• 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

Publications

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