Using programming language theory to make automatic differentiation sound and efficient

This paper discusses a new Automatic Differentiation (AD) system that correctly and automatically accepts nested and dynamic use of the AD operators, without any manual intervention. The system is based on a new formulation of AD as highly generalized firstclass citizens in a λ- calculus, which is briefly described. Because the λ-calculus is the basis for modern programming-language implementation techniques, integration of AD into the λ-calculus allows AD to be integrated into an aggressive compiler. We exhibit a research compiler which does this integration. Using novel analysis techniques, it accepts source code involving free use of a first-class forward AD operator and generates object code which attains numerical performance comparable to, or better than, the most aggressive existing AD systems