Formalized Correctness Proofs of Automatic Differentiation in Coq

Abstract

In this thesis, we give a formalized proof of correctness of both a ubiquitous forward-mode and a continuation-based pseudo-reverse-mode automatic differentiation algorithm. We repeatedly do this using logical relations arguments accompanied by simple but effective language representations and denotational semantics. We also discuss and prove sound various program transformations, which in the context of efficient code generation for automatic differentiation, let forward-mode approach the performance of reverse-mode algorithms. Finally, we make preliminary steps towards a formalized proof of correctness of a real combinator-based reverse-mode algorithm.