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.

@article{paperbot1581,
  title = {Provably correct, asymptotically efficient, higher-order reverse-mode automatic differentiation},
  author = {Faustyna Krawiec and Simon Peyton Jones and Neel Krishnaswami and Tom Ellis and Richard A. Eisenberg and Andrew Fitzgibbon},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {POPL},
  year = {2022},
  doi = {10.1145/3498710}
}