27 citations · 53 across the 14 of their papers we have counts for
16 papers
Adequate Losses via Quantitative Linear Logic
Matteo Capucci, Robert Atkey, Charles Grellois +2
As neural components are increasingly embedded in existing symbolic software -- including safety-critical systems -- the question arises of how to specify and enforce the safety of…
Data Provenance as Automatic Differentiation
Robert Atkey, Roly Perera
Automatic differentiation (AD) computes the derivative of a program alongside the program itself, as a linear map between tangent spaces, propagated forwards or backwards along an…
A Semantic Proof of Generalised Cut Elimination for Deep Inference
Robert Atkey, Wen Kokke
Multiplicative-Additive System Virtual (MAV) is a logic that extends Multiplicative-Additive Linear Logic with a self-dual non-commutative operator expressing the concept of "befor…
Compiling High-Level Neural Network Specifications into VNN-LIB Queries
Matthew L. Daggitt, Wen Kokke, Robert Atkey
The formal verification of traditional software has been revolutionised by verification-orientated languages such as Dafny and F* which enable developers to write high-level specif…
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs
Matthew L. Daggitt, Wen Kokke, Robert Atkey +3
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodolog…
Polynomial Time and Dependent Types
Robert Atkey
We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one syste…