Dieses Dokument darf im Rahmen von § 53 UrhG zum eigenen Gebrauch kostenfrei heruntergeladen, gelesen, gespeichert und ausgedruckt, aber nicht im Internet bereitgestellt oder an Außenstehende weitergegeben werden.This document may be downloaded, read, stored and printed for your own use within the limits of § 53 UrhG but it may not be distributed via the internet or passed on to external parties.Lucatelli Nunes, FernandoVákár, Matthijs2024-10-172024-10-172023https://oa.tib.eu/renate/handle/123456789/16994https://doi.org/10.34657/16016We present a simple technique for semantic, open logical relations arguments about languages with recursive types, which, as we show, follows from a principled foundation in categorical semantics. We demonstrate how it can be used to give a very straightforward proof of correctness of practical forward- and reverse-mode dual numbers style automatic differentiation (AD) on ML-family languages. The key idea is to combine it with a suitable open logical relations technique for reasoning about differentiable partial functions (a suitable lifting of the partiality monad to logical relations), which we introduce.engRecursive TypesLogical RelationsAutomatic differentiationProgramming LanguagesFunctional ProgrammingDenotational SemanticsRecursionProgram TransformationsEnriched Category Theory510Report