# Reverse AD at Higher Types: Pure, Principled and Denotationally Correct

arXiv: https://arxiv.org/abs/2007.05283 · HTML: https://mlsanity.com/paper/2007.05283/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Jul 2020.

## Built on by (most cited first, 3 of 3)

- [On the Correctness of Automatic Differentiation for Neural Networks with Machine-Representable Parameters](https://mlsanity.com/paper/2301.13370/) (2023)
- [Functorial String Diagrams for Reverse-Mode Automatic Differentiation](https://mlsanity.com/paper/2107.13433/) (2021)
- [Combinatory Adjoints and Differentiation](https://mlsanity.com/paper/2207.00847/) (2022)

## Abstract (arXiv)

We show how to define forward- and reverse-mode automatic differentiation source-code transformations or on a standard higher-order functional language. The transformations generate purely functional code, and they are principled in the sense that their definition arises from a categorical universal property. We give a semantic proof of correctness of the transformations. In their most elegant formulation, the transformations generate code with linear types. However, we demonstrate how the transformations can be implemented in a standard functional language without sacrificing correctness. To do so, we make use of abstract data types to represent the required linear types, e.g. through the use of a basic module system.