A lambda-Calculus for Resource Separation. - Robert Atkey (ICALP, 2004)

CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. - Robert Atkey (TYPES, 2007)

What is a Categorical Model of Arrows? - Robert Atkey (MSFP@ICALP, 2008)

Algebras for Parameterised Monads. - Robert Atkey (CALCO, 2009)

Unembedding domain-specific languages. - Robert Atkey; Sam Lindley; Jeremy Yallop (Haskell, 2009)

Syntax for Free: Representing Syntax with Binding Using Parametricity. - Robert Atkey (TLCA, 2009)

Parameterised notions of computation. - Robert Atkey (J. Funct. Program., 2009)

Refinement and Term Synthesis in Loop Invariant Generation. - Ewen Maclean; Andrew Ireland; Lucas Dixon; Robert Atkey (WING@ETAPS/IJCAR, 2010)

Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode. - David Aspinall 001; Robert Atkey; Kenneth MacKenzie; Donald Sannella (TGC, 2010)

When Is a Type Refinement an Inductive Type? - Robert Atkey; Patricia Johann; Neil Ghani (FoSSaCS, 2011)

Amortised Resource Analysis with Separation Logic - Robert Atkey (Log. Methods Comput. Sci., 2011)

Relational Parametricity for Higher Kinds. - Robert Atkey (CSL, 2012)

Fibrational Induction Meets Effects. - Robert Atkey; Neil Ghani; Bart Jacobs 001; Patricia Johann (FoSSaCS, 2012)

The Semantics of Parsing with Semantic Actions. - Robert Atkey (LICS, 2012)

Refining Inductive Types - Robert Atkey; Patricia Johann; Neil Ghani (Log. Methods Comput. Sci., 2012)

Productive coprogramming with guarded recursion. - Robert Atkey; Conor McBride (ICFP, 2013)

Abstraction and invariance for algebraically indexed types. - Robert Atkey; Patricia Johann; Andrew Kennedy (POPL, 2013)

From parametricity to conservation laws, via Noether's theorem. - Robert Atkey (POPL, 2014)

A relationally parametric model of dependent type theory. - Robert Atkey; Neil Ghani; Patricia Johann (POPL, 2014)

Models for Polymorphism over Physical Dimension. - Robert Atkey; Neil Ghani; Fredrik Nordvall Forsberg; Timothy Revell; Sam Staton (TLCA, 2015)

ThreadSafe: Static Analysis for Java Concurrency. - Robert Atkey; Donald Sannella (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

Interleaving data and effects. - Robert Atkey; Patricia Johann (J. Funct. Program., 2015)

Conflation Confers Concurrency. - Robert Atkey; Sam Lindley; J. Garrett Morris (A List of Successes That Can Change the World, 2016)

Observed Communication Semantics for Classical Processes. - Robert Atkey (ESOP, 2017)

Continuation Passing Style for Effect Handlers. - Daniel Hillerström; Sam Lindley; Robert Atkey; K. C. Sivaramakrishnan (FSCD, 2017)

Strategy Preserving Compilation for Parallel Functional Code. - Robert Atkey; Michel Steuwer; Sam Lindley; Christophe Dubach (CoRR, 2017)

Syntax and Semantics of Quantitative Type Theory. - Robert Atkey (LICS, 2018)

A type and scope safe universe of syntaxes with binding: their semantics and proofs. - Guillaume Allais; Robert Atkey; James Chapman 001; Conor McBride; James McKinna (Proc. ACM Program. Lang., 2018)

Dijkstra monads for all. - Kenji Maillard; Danel Ahman; Robert Atkey; Guido Martínez; Catalin Hritcu; Exequiel Rivas; Éric Tanter (Proc. ACM Program. Lang., 2019)

Neural Networks, Secure by Construction - An Exploration of Refinement Types. - Wen Kokke; Ekaterina Komendantskaya; Daniel Kienitz; Robert Atkey; David Aspinall 001 (APLAS, 2020)

A Linear Algebra Approach to Linear Metatheory. - James Wood; Robert Atkey (Linearity&TLLA@IJCAR-FSCD, 2020)

Compositional Game Theory, Compositionally. - Robert Atkey; Bruno Gavranovic; Neil Ghani; Clemens Kupke; Jérémy Ledent; Fredrik Nordvall Forsberg (ACT, 2020)

Effect handlers via generalised continuations. - Daniel Hillerström; Sam Lindley; Robert Atkey (J. Funct. Program., 2020)

A Framework for Substructural Type Systems. - James Wood; Robert Atkey (ESOP, 2022)

Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers. - Matthew L. Daggitt; Wen Kokke; Robert Atkey; Luca Arnaboldi 001; Ekaterina Komendantskaya (CoRR, 2022)

The Vehicle Tutorial: Neural Network Verification with Vehicle. - Matthew L. Daggitt; Wen Kokke; Ekaterina Komendantskaya; Robert Atkey; Luca Arnaboldi 001; Natalia Slusarz; Marco Casadio; Ben Coke; Jeonghyeon Lee (FoMLAS@CAV, 2023)

Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. - Matthew L. Daggitt; Robert Atkey; Wen Kokke; Ekaterina Komendantskaya; Luca Arnaboldi 001 (CPP, 2023)

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. - Matthew L. Daggitt; Wen Kokke; Robert Atkey; Natalia Slusarz; Luca Arnaboldi 001; Ekaterina Komendantskaya (CoRR, 2024)

Efficient compilation of expressive problem space specifications to neural network solvers. - Matthew L. Daggitt; Wen Kokke; Robert Atkey (CoRR, 2024)

A Semantic Proof of Generalised Cut Elimination for Deep Inference. - Robert Atkey; Wen Kokke (CoRR, 2024)

Polynomial Time and Dependent Types. - Robert Atkey (Proc. ACM Program. Lang., 2024)

Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs (Invited Talk). - Matthew L. Daggitt; Wen Kokke; Robert Atkey; Ekaterina Komendantskaya; Natalia Slusarz; Luca Arnaboldi 001 (FSCD, 2025)