Automatic Differentiation for ML-family languages: correctness via logical relations

Fernando Lucatelli Nunes, Matthijs Vákár

We give a simple, direct and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by wo…