Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation - Krawiec, Faustyna; Krishnaswami, Neel; Peyton Jones, Simon; Ellis, Tom; Fitzgibbon, Andrew; Eisenberg, Richard (POPL 2022, 2021)
In this paper, we give a simple and efficient implementation of reverse-mode automatic differentiation, which both extends easily to higher-order functions, and has run time and memory consumption linear in the run time of the original program. In addition to a formal description of the translation, we also describe an implementation of this algorithm, and prove its correctness by means of a logical relations argument. Here is a video of Simon giving a talk about the paper.