Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
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 aski...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2023-10-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/8851/pdf |
| _version_ | 1797268519963852800 |
|---|---|
| author | Paulo Emílio de Vilhena François Pottier |
| author_facet | Paulo Emílio de Vilhena François Pottier |
| author_sort | Paulo Emílio de Vilhena |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:33:47Z |
| format | Article |
| id | doaj.art-c3eb8936345649fda3bf96782f94e5cb |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:47Z |
| publishDate | 2023-10-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-c3eb8936345649fda3bf96782f94e5cb2024-03-08T10:43:58ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742023-10-01Volume 19, Issue 410.46298/lmcs-19(4:5)20238851Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD LibraryPaulo Emílio de VilhenaFrançois PottierWe 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.https://lmcs.episciences.org/8851/pdfcomputer science - logic in computer sciencecomputer science - programming languages |
| spellingShingle | Paulo Emílio de Vilhena François Pottier Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library Logical Methods in Computer Science computer science - logic in computer science computer science - programming languages |
| title | Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library |
| title_full | Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library |
| title_fullStr | Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library |
| title_full_unstemmed | Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library |
| title_short | Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library |
| title_sort | verifying an effect handler based define by run reverse mode ad library |
| topic | computer science - logic in computer science computer science - programming languages |
| url | https://lmcs.episciences.org/8851/pdf |
| work_keys_str_mv | AT pauloemiliodevilhena verifyinganeffecthandlerbaseddefinebyrunreversemodeadlibrary AT francoispottier verifyinganeffecthandlerbaseddefinebyrunreversemodeadlibrary |