6 citations · 15 across the 8 of their papers we have counts for
9 papers
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…
Separating Sessions Smoothly
Simon Fowler, Wen Kokke, Ornela Dardha +2
This paper introduces Hypersequent GV (HGV), a modular and extensible core calculus for functional programming with session types that enjoys deadlock freedom, confluence, and stro…
Neural Network Robustness as a Verification Property: A Principled Case Study
Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt +4
Neural networks are very successful at detecting patterns in noisy data, and have become the technology of choice in many fields. However, their usefulness is hampered by their sus…
Deadlock-Free Session Types in Linear Haskell
Wen Kokke, Ornela Dardha
Priority Sesh is a library for session-typed communication in Linear Haskell which offers strong compile-time correctness guarantees. Priority Sesh offers two deadlock-free APIs fo…
Prioritise the Best Variation
Wen Kokke, Ornela Dardha
Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical…
Featherweight Go
Robert Griesemer, Raymond Hu, Wen Kokke +5
We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structura…
Formalising Type-Logical Grammars in Agda
Wen Kokke
In recent years, the interest in using proof assistants to formalise and reason about mathematics and programming languages has grown. Type-logical grammars, being closely related…