| dc.description.abstract | Automatic Differentiation (AD) is a technique for efficiently calculating derivatives of functions represented as programs.
Efficient CHAD, presented by Smeding (2024),
is an implementation of an AD algorithm for a first-order functional source language.
This algorithm has desirable properties.
Its implementation is made in Agda, a dependently typed functional programming language and proof assistant.
In this thesis, we formally prove the correctness of efficient CHAD in Agda.
For the specification, we relate efficient CHAD to semantic differentiation,
which we encode using postulates.
Additionally, we extend efficient CHAD to work on a higher-order source language.
For this higher-order version of efficient CHAD,
we lay the foundation of a correctness proof,
but leave the full proof as future work. | |
