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

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

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

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

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

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

Polynomial Time and Dependent Types. - Atkey, Robert (CoRR, 2023)

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

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

A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. - Allais, Guillaume; Atkey, Robert; Chapman, James; McBride, Conor; McKinna, James (J. Funct. Program., 2021)

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

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

A Linear Algebra Approach to Linear Metatheory. - Wood, James; Atkey, Robert (2020)

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

A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. - Allais, Guillaume; Atkey, Robert; Chapman, James; McBride, Conor; McKinna, James (CoRR, 2020)

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

Dijkstra Monads for All. - Maillard, Kenji; Ahman, Danel; Atkey, Robert; Martínez, Guido; Hritcu, Catalin; Rivas, Exequiel; Tanter, Éric (CoRR, 2019)

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

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

Proceedings of the 7th Workshop on Mathematically Structured Functional Programming, MSFP@FSCD 2018, Oxford, UK, 8th July 2018. (2018)

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

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

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

Conflation Confers Concurrency. - Atkey, Robert; Lindley, Sam; Morris, J. Garrett (2016)

Proceedings 6th Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2016, Eindhoven, Netherlands, 8th April 2016. (2016)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Amortised Resource Analysis with Separation Logic. - Atkey, Robert (2010)

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

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

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

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

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

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

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

Parameterised Notions of Computation. - Atkey, Robert (2006)

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