Paulo Emílio de Vilhena ; François Pottier - Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

lmcs:8851 - Logical Methods in Computer Science, October 23, 2023, Volume 19, Issue 4 - https://doi.org/10.46298/lmcs-19(4:5)2023
Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD LibraryArticle

Authors: Paulo Emílio de Vilhena ; François Pottier

    We apply program verification technology to the problem of specifying and verifying automatic differentiation (AD) algorithms. We focus on define-by-run, a style of AD where the program that must be differentiated is executed and monitored by the automatic differentiation algorithm. We begin by asking, "what is an implementation of AD?" and "what does it mean for an implementation of AD to be correct?" We answer these questions both at an informal level, in precise English prose, and at a formal level, using types and logical assertions. After answering these broad questions, we focus on a specific implementation of AD, which involves a number of subtle programming-language features, including dynamically allocated mutable state, first-class functions, and effect handlers. We present a machine-checked proof, expressed in a modern variant of Separation Logic, of its correctness. We view this result as an advanced exercise in program verification, with potential future applications to the verification of more realistic automatic differentiation systems and of other software components that exploit delimited-control effects.


    Volume: Volume 19, Issue 4
    Published on: October 23, 2023
    Accepted on: July 28, 2023
    Submitted on: December 15, 2021
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    Consultation statistics

    This page has been seen 735 times.
    This article's PDF has been downloaded 209 times.