5 citations · 12 across the 8 of their papers we have counts for
8 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…
Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection
Artjoms Šinkarovs, Jesper Cockx
Dependently-typed host languages empower users to verify a wide range of properties of embedded languages and programs written in them. Designers of such embedded languages are fac…
Multi-dimensional Arrays with Levels
Artjoms {Š}inkarovs
We explore a data structure that generalises rectangular multi-dimensional arrays. The shape of an n-dimensional array is typically given by a tuple of n natural numbers. Each elem…
Array Languages Make Neural Networks Fast
Artjoms Šinkarovs, Hans-Nikolai Vießmann, Sven-Bodo Scholz
Modern machine learning frameworks are complex: they are typically organised in multiple layers each of which is written in a different language and they depend on a number of exte…
A Lambda Calculus for Transfinite Arrays: Unifying Arrays and Streams
Artjoms Sinkarovs, Sven-Bodo Scholz
Array programming languages allow for concise and generic formulations of numerical algorithms, thereby providing a huge potential for program optimisation such as fusion, parallel…