Robert Atkey

Publication Activity (10 Years)

Years Active: 2004-2024
Publications (10 Years): 23

Top Topics

Top Venues

Proc. ACM Program. Lang.

J. Funct. Program.

Publications

Matthew L. Daggitt, Wen Kokke, Robert Atkey, Natalia Slusarz, Luca Arnaboldi, Ekaterina Komendantskaya
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. CoRR (2024)
Robert Atkey, Wen Kokke
A Semantic Proof of Generalised Cut Elimination for Deep Inference. CoRR (2024)
Robert Atkey
Polynomial Time and Dependent Types. Proc. ACM Program. Lang. 8 (POPL) (2024)
Matthew L. Daggitt, Wen Kokke, Robert Atkey
Efficient compilation of expressive problem space specifications to neural network solvers. CoRR (2024)
Matthew L. Daggitt, Wen Kokke, Ekaterina Komendantskaya, Robert Atkey, Luca Arnaboldi, Natalia Slusarz, Marco Casadio, Ben Coke, Jeonghyeon Lee
The Vehicle Tutorial: Neural Network Verification with Vehicle. FoMLAS@CAV (2023)
Robert Atkey
Polynomial Time and Dependent Types. CoRR (2023)
Matthew L. Daggitt, Robert Atkey, Wen Kokke, Ekaterina Komendantskaya, Luca Arnaboldi
Compiling Higher-Order Specifications to SMT Solvers: How to Deal with Rejection Constructively. CPP (2023)
James Wood, Robert Atkey
A Framework for Substructural Type Systems. ESOP (2022)
Matthew L. Daggitt, Wen Kokke, Robert Atkey, Luca Arnaboldi, Ekaterina Komendantskaya
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers. CoRR (2022)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program. 31 (2021)
Robert Atkey, Bruno Gavranovic, Neil Ghani, Clemens Kupke, Jérémy Ledent, Fredrik Nordvall Forsberg
Compositional Game Theory, Compositionally. ACT (2020)
Wen Kokke, Ekaterina Komendantskaya, Daniel Kienitz, Robert Atkey, David Aspinall
Neural Networks, Secure by Construction - An Exploration of Refinement Types. APLAS (2020)
James Wood, Robert Atkey
A Linear Algebra Approach to Linear Metatheory. CoRR (2020)
Daniel Hillerström, Sam Lindley, Robert Atkey
Effect handlers via generalised continuations. J. Funct. Program. 30 (2020)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs. CoRR (2020)
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
Dijkstra monads for all. Proc. ACM Program. Lang. 3 (ICFP) (2019)
Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Catalin Hritcu, Exequiel Rivas, Éric Tanter
Dijkstra Monads for All. CoRR (2019)
Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, James McKinna
A type and scope safe universe of syntaxes with binding: their semantics and proofs. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Robert Atkey
Syntax and Semantics of Quantitative Type Theory. LICS (2018)
Daniel Hillerström, Sam Lindley, Robert Atkey, K. C. Sivaramakrishnan
Continuation Passing Style for Effect Handlers. FSCD (2017)
Robert Atkey
Observed Communication Semantics for Classical Processes. ESOP (2017)
Robert Atkey, Michel Steuwer, Sam Lindley, Christophe Dubach
Strategy Preserving Compilation for Parallel Functional Code. CoRR (2017)
Robert Atkey, Sam Lindley, J. Garrett Morris
Conflation Confers Concurrency. A List of Successes That Can Change the World (2016)
Robert Atkey, Donald Sannella
ThreadSafe: Static Analysis for Java Concurrency. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015)
Robert Atkey, Patricia Johann
Interleaving data and effects. J. Funct. Program. 25 (2015)
Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton
Models for Polymorphism over Physical Dimension. TLCA (2015)
Robert Atkey, Neil Ghani, Patricia Johann
A relationally parametric model of dependent type theory. POPL (2014)
Robert Atkey
From parametricity to conservation laws, via Noether's theorem. POPL (2014)
Robert Atkey, Patricia Johann, Andrew Kennedy
Abstraction and invariance for algebraically indexed types. POPL (2013)
Robert Atkey, Conor McBride
Productive coprogramming with guarded recursion. ICFP (2013)
Robert Atkey
Relational Parametricity for Higher Kinds. CSL (2012)
Robert Atkey, Patricia Johann, Neil Ghani
Refining Inductive Types Log. Methods Comput. Sci. 8 (2) (2012)
Robert Atkey, Neil Ghani, Bart Jacobs, Patricia Johann
Fibrational Induction Meets Effects. FoSSaCS (2012)
Robert Atkey
The Semantics of Parsing with Semantic Actions. LICS (2012)
Robert Atkey
Amortised Resource Analysis with Separation Logic Log. Methods Comput. Sci. 7 (2) (2011)
Robert Atkey, Patricia Johann, Neil Ghani
When Is a Type Refinement an Inductive Type? FoSSaCS (2011)
Robert Atkey
What is a Categorical Model of Arrows? Electron. Notes Theor. Comput. Sci. 229 (5) (2011)
Ewen Maclean, Andrew Ireland, Lucas Dixon, Robert Atkey
Refinement and Term Synthesis in Loop Invariant Generation. WING@ETAPS/IJCAR (2010)
David Aspinall, Robert Atkey, Kenneth MacKenzie, Donald Sannella
Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode. TGC (2010)
Robert Atkey
Amortised Resource Analysis with Separation Logic. ESOP (2010)
Robert Atkey
Algebras for Parameterised Monads. CALCO (2009)
Robert Atkey
Parameterised notions of computation. J. Funct. Program. 19 (3-4) (2009)
Robert Atkey, Sam Lindley, Jeremy Yallop
Unembedding domain-specific languages. Haskell (2009)
Robert Atkey
Syntax for Free: Representing Syntax with Binding Using Parametricity. TLCA (2009)
Robert Atkey
CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. TYPES (2007)
Robert Atkey
Parameterised Notions of Computation. MSFP@MPC (2006)
Robert Atkey
A lambda-Calculus for Resource Separation. ICALP (2004)