Robert Atkey

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