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
POPL 2024 - A Semantic Proof of Generalised Cut Elimination for Deep Inference
MFPS LX, 2024 - 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