4 papers
When Agda met Vampire
Artjoms Å inkarovs, Michael Rawson
Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in…
Comparing Parallel Functional Array Languages: Programming and Performance
David van Balen, Tiziano De Matteis, Clemens Grelck +12
Parallel functional array languages are an emerging class of programming languages that promise to combine low-effort parallel programming with good performance and performance por…
Neural Network Verification is a Programming Language Challenge
Lucas C. Cordeiro, Matthew L. Daggitt, Julien Girard-Satabin +8
Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while pr…
Correctness is Demanding, Performance is Frustrating
Artjoms Sinkarovs, Thomas Koopman, Sven-Bodo Scholz
In this paper we demonstrate a technique for developing high performance applications with strong correctness guarantees. We use a theorem prover to derive a high-level specificati…