Source author record

Robert Atkey

Robert Atkey appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Programming Languages Machine Learning math.CT

Catalog footprint

What is connected

6works

4topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2022arXiv

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 networks with hundreds of thousands of nodes. In theory this opens the door to the verification of larger control systems that make use of neural network components. However, although work has managed to incorporate the results of these verifiers to prove larger properties of individual systems, there is currently no general methodology for bridging the gap between verifiers and interactive theorem provers (ITPs). In this paper we present Vehicle, our solution to this problem. Vehicle is equipped with an expressive domain specific language for stating neural network specifications which can be compiled to both verifiers and ITPs. It overcomes previous issues with maintainability and scalability in similar ITP formalisations by using a standard ONNX file as the single canonical representation of the network. We demonstrate its utility by using it to connect the neural network verifier Marabou to Agda and then formally verifying that a car steered by a neural network never leaves the road, even in the face of an unpredictable cross wind and imperfect sensors. The network has over 20,000 nodes, and therefore this proof represents an improvement of 3 orders of magnitude over prior proofs about neural network enhanced systems in ITPs.

preprint2021arXiv

A Linear Algebra Approach to Linear Metatheory

Linear typed $λ$-calculi are more delicate than their simply typed siblings when it comes to metatheoretic results like preservation of typing under renaming and substitution. Tracking the usage of variables in contexts places more constraints on how variables may be renamed or substituted. We present a methodology based on linear algebra over semirings, extending McBride's kits and traversals approach for the metatheory of syntax with binding to linear usage-annotated terms. Our approach is readily formalisable, and we have done so in Agda.

preprint2021arXiv

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 build new Arrows from old. We model equilibria as a bimodule over an Arrow and define an operator to build a new Arrow from such a bimodule over an existing Arrow. We also model strategies as graded Arrows and define an operator which builds a new Arrow by taking the colimit of a graded Arrow. A final operator builds a graded Arrow from a graded bimodule. We use this compositional approach to CGT to show how known and previously unknown variants of open games can be proven to form symmetric monoidal categories.

preprint2016arXiv

Proceedings 6th Workshop on Mathematically Structured Functional Programming

The sixth workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without arrows? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. The sixth workshop on Mathematically Structured Functional Programming was held on 8th April 2016 as a part of ETAPS 2016 in Eindhoven, the Netherlands. There were five contributed talks and one invited talk.

preprint2012arXiv

Refining Inductive Types

Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the N-indexed type of vectors refines lists by their lengths. Other data types may be refined in similar ways, but programmers must produce purpose-specific refinements on an ad hoc basis, developers must anticipate which refinements to include in libraries, and implementations must often store redundant information about data and their refinements. In this paper we show how to generically derive inductive characterisations of refinements of inductive types, and argue that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. Our characterisations also ensure that standard techniques for programming with and reasoning about inductive types are applicable to refinements, and that refinements can themselves be further refined.

preprint2011arXiv

Amortised Resource Analysis with Separation Logic

Type-based amortised resource analysis following Hofmann and Jost---where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline---have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative pointer-manipulating languages by embedding a logic of resources, based on the affine intuitionistic Logic of Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the consumable resources associated with each member of the structure. We present the logic on a small imperative language, based on Java bytecode, with procedures and mutable heap. We have formalised the logic and its soundness property within the Coq proof assistant and extracted a certified verification condition generator. We also describe an proof search procedure that allows generated verification conditions to be discharged while using linear programming to infer consumable resource annotations. We demonstrate the logic on some examples, including proving the termination of in-place list reversal on lists with cyclic tails.