| 2025 | FSCD | 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 |
| 2023 | CAV | The Vehicle Tutorial: Neural Network Verification with Vehicle. | Matthew L. Daggitt, Wen Kokke, Ekaterina Komendantskaya, Robert Atkey, Luca Arnaboldi, Natalia Slusarz, Marco Casadio, Ben Coke, Jeonghyeon Lee |
| 2023 | CPP | Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. | Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi |
| 2022 | ESOP | A Framework for Substructural Type Systems. | James Wood, Robert Atkey |
| 2020 | APLAS | Neural Networks, Secure by Construction - An Exploration of Refinement Types. | Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall |
| 2018 | LICS | Syntax and Semantics of Quantitative Type Theory. | Robert Atkey |
| 2017 | ESOP | Observed Communication Semantics for Classical Processes. | Robert Atkey |
| 2014 | POPL | From parametricity to conservation laws, via Noether's theorem. | Robert Atkey |
| 2014 | POPL | A relationally parametric model of dependent type theory. | Robert Atkey, Neil Ghani, Patricia Johann |
| 2013 | ICFP | Productive coprogramming with guarded recursion. | Robert Atkey, Conor McBride |
| 2013 | POPL | Abstraction and invariance for algebraically indexed types. | Robert Atkey, Patricia Johann, Andrew Kennedy |
| 2012 | CSL | Relational Parametricity for Higher Kinds. | Robert Atkey |
| 2012 | FOSSACS | Fibrational Induction Meets Effects. | Robert Atkey, Neil Ghani, Bart Jacobs, Patricia Johann |
| 2012 | LICS | The Semantics of Parsing with Semantic Actions. | Robert Atkey |
| 2011 | FOSSACS | When Is a Type Refinement an Inductive Type? | Robert Atkey, Patricia Johann, Neil Ghani |
| 2010 | CADE | Refinement and Term Synthesis in Loop Invariant Generation. | Ewen Maclean, Andrew Ireland, Lucas Dixon, Robert Atkey |
| 2010 | ESOP | Amortised Resource Analysis with Separation Logic. | Robert Atkey |
| 2009 | CALCO | Algebras for Parameterised Monads. | Robert Atkey |
| 2009 | HASKELL | Unembedding domain-specific languages. | Robert Atkey, Sam Lindley, Jeremy Yallop |
| 2006 | MPC | Parameterised Notions of Computation. | Robert Atkey |
| 2004 | ICALP | A lambda-Calculus for Resource Separation. | Robert Atkey |