Abstract
Automatic differentiation plays a prominent role in scientific computing andin modern machine learning, often in the context of powerful programmingsystems. The relation of the various embodiments of automatic differentiationto the mathematical notion of derivative is not always entirelyclear---discrepancies can arise, sometimes inadvertently. In order to studyautomatic differentiation in such programming contexts, we define a small butexpressive programming language that includes a construct for reverse-modedifferentiation. We give operational and denotational semantics for thislanguage. The operational semantics employs popular implementation techniques,while the denotational semantics employs notions of differentiation familiarfrom real analysis. We establish that these semantics coincide.