Paulo Emílio de Vilhena

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

2023 · Logical Methods in Computer Science

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 …