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
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