Zobrazeno 1 - 10
of 67
pro vyhledávání: '"Atkey, Robert"'
Autor:
Atkey, Robert, Kokke, Wen
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 "sequencing". MAV is also an extenson of the the logic Basic Sys
Externí odkaz:
http://arxiv.org/abs/2404.06233
Recent work has described the presence of the embedding gap in neural network verification. On one side of the gap is a high-level specification about the network's behaviour, written by a domain expert in terms of the interpretable problem space. On
Externí odkaz:
http://arxiv.org/abs/2402.01353
Autor:
Daggitt, Matthew L., Kokke, Wen, Atkey, Robert, Slusarz, Natalia, Arnaboldi, Luca, Komendantskaya, Ekaterina
Neuro-symbolic programs -- programs containing both machine learning components and traditional symbolic code -- are becoming increasingly widespread. However, we believe that there is still a lack of a general methodology for verifying these program
Externí odkaz:
http://arxiv.org/abs/2401.06379
Autor:
Atkey, Robert
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 construction of iterable data, and one, based on the
Externí odkaz:
http://arxiv.org/abs/2307.09145
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 thi
Externí odkaz:
http://arxiv.org/abs/2202.05207
Autor:
Atkey, Robert, Gavranović, Bruno, Ghani, Neil, Kupke, Clemens, Ledent, Jérémy, Forsberg, Fredrik Nordvall
Publikováno v:
EPTCS 333, 2021, pp. 198-214
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 b
Externí odkaz:
http://arxiv.org/abs/2101.12045
Autor:
Wood, James, Atkey, Robert
Publikováno v:
EPTCS 353, 2021, pp. 195-212
Linear typed $\lambda$-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
Externí odkaz:
http://arxiv.org/abs/2005.02247
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 substitution, typing contexts, runtime environments, and so on.
Externí odkaz:
http://arxiv.org/abs/2001.11001
Autor:
Maillard, Kenji, Ahman, Danel, Atkey, Robert, Martinez, Guido, Hritcu, Catalin, Rivas, Exequiel, Tanter, Éric
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 specification monad. We prove that any monad morphism between a c
Externí odkaz:
http://arxiv.org/abs/1903.01237
Autor:
Atkey, Robert, Lindley, Sam
Publikováno v:
EPTCS 275, 2018
The seventh 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
Externí odkaz:
http://arxiv.org/abs/1807.03732