2024/06/14 by Artjoms Šinkarovs, Thomas Koopman, Sinkarovs, Artjoms +3
Computer Science · #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Software System Performance and Reliability #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2406.10405
openalex publication_date 2024/06/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 specification of the application that includes correctness invariants of our choice. After that, within the same theorem prover, we implement an extraction of the specified application into a high-performance language of our choice. Concretely, we are using Agda to specify a framework for automatic differentiation (reverse mode) that is focused on index-safe tensors. This framework comes with an optimiser for tensor expressions and the ability to translate these expressions into SaC and C. We specify a canonical convolutional neural network within the proposed framework, compute the derivatives needed for the training phase and then demonstrate that the generated code matches the performance of hand-written code when running on a multi-core machine.