Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

DOI10.46298/LMCS-19(4:5)2023MaRDI QIDQ6178671zbMATH OpenFDO

Authors Paulo Emílio de Vilhena, François Pottier

Publication date 16 January 2024

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2112.07292

zbMATH Keywords

program verificationseparation logicautomatic differentiationeffect handlers

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Abstract: 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.

Recommendations

• Reverse AD at higher types: pure, principled and denotationally correct
• Correctness of automatic differentiation via diffeologies and categorical gluing
• On formal certification of AD transformations

Cites work

• scientific article; zbMATH DE number 3562487 (Why is no real title available?)
• scientific article; zbMATH DE number 6982909 (Why is no real title available?)
• scientific article; zbMATH DE number 7566054 (Why is no real title available?)
• scientific article; zbMATH DE number 7650831 (Why is no real title available?)
• An introduction to algebraic effects and handlers (invited tutorial paper)
• Beautiful differentiation
• Correctness of automatic differentiation via diffeologies and categorical gluing
• Effect handlers via generalised continuations
• Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
• Evaluating Derivatives
• Exception Handling in CLU
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Functional differentiation of computer programs
• Functional differentiation of computer programs
• Handlers of Algebraic Effects
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Koka: programming with row polymorphic effect types
• Modular verification of programs with effects and effect handlers in Coq
• Modular verification of programs with effects and effects handlers
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• Programming with algebraic effects and handlers
• Reverse AD at higher types: pure, principled and denotationally correct
• Separation Logic Tutorial
• Shallow effect handlers
• There and back again
• Typed Tagless Final Interpreters

This page was built for publication: Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6178671)