## About

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.

## Posts

- 2023-11-02:
More Data Types with Negation at Fun in the REPL - 2023-01-17:
Compiling higher-order specifications to SMT solvers - 2023-01-16:
Simple semantics for defaults in Catala - 2023-01-15:
Data types with Negation - 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:
Abstraction and Invariance for Algebraically Indexed Types - 2012-11-07:
Theorems for Free - 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.

- Polynomial Time and Dependent Types
*ArXiv 2023* - Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively
*CPP 2023* - Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
*ArXiv 2022* - A Framework for Substructural Type Systems
*ESOP 2022* - Data types with Negation (Talk Abstract)
*MSFP 2022 (Talk Abstract)* - 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* - Context Constrained Computation
*TyDe 2018 (Extended Abstract)* - A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
*ICFP 2018* - The Syntax and Semantics of Quantitative Type Theory
*LICS 2018* - Compiling Parallel Functional Code with Data Parallel Idealised Algol
*ArXiv (2017)* - Observed Communication Semantics for Classical Processes
*ESOP 2017* - Continuation Passing Style for Effect Handlers
*FSCD 2017* - Conflation Confers Concurrency
*WadlerFest 2016* - Interleaving data and effects
*Journal of Functional Programming, 2015* - Models for Polymorphism over Physical Dimensions
*TLCA 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* - Refining Inductive Types
*Logical Methods in Computer Science, 2012* - Fibrational Induction Meets Effects
*FoSSaCS 2012* - The Semantics of Parsing with Semantic Actions
*LICS 2012* - Relational Parametricity for Higher Kinds
*CSL 2012* - Amortised Resource Analysis with Separation Logic
*Logical Methods in Computer Science, 2011* - When Is a Type Refinement an Inductive Type?
*FoSSaCS 2011* - Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode
*TGC 2010* - Amortised Resource Analysis with Separation Logic
*ESOP 2010* - Parameterised notions of computation
*Journal of Functional Programming, 2009* - A Deep Embedding of Parametric Polymorphism in Coq
*WMM 2009* - Unembedding domain-specific languages
*Haskell Symposium 2009* - Syntax for Free: Representing Syntax with Binding Using Parametricity
*TLCA 2009* - Algebras for Parameterised Monads
*CALCO 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* - Substructural Simple Type Theories for Separation and In-place Update
*PhD Thesis* - Parameterised Notions of Computation
*MSFP 2006* - A 𝜆-Calculus for Resource Separation
*ICALP 2004*