Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying...
Compiling High-Level Neural Network Specifications into VNN-LIB Queries
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 specifications that...
Polynomial Time and Dependent Types
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 system that disallows...
A Semantic Proof of Generalised Cut Elimination for Deep Inference
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 "before" or...
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
Verification of neural networks is currently a hot topic in automated theorem proving. Progress has been rapid and there are now a wide range of tools available that can verify properties of...
A Type and Scope Safe Universe of Syntaxes with Binding: Their Semantics and Proofs
Almost every programming language's syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of $\alpha$-equivalence, capture-avoiding...
Dijkstra Monads for All
This paper proposes a general semantic framework for verifying programs with arbitrary monadic side-effects using Dijkstra monads, which we define as monad-like structures indexed by a...
Compositional Game Theory, Compositionally
We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to...
Strategy Preserving Compilation for Parallel Functional Code
Graphics Processing Units (GPUs) and other parallel devices are widely available and have the potential for accelerating a wide class of algorithms. However, expert programming skills are required...