Logical Relations for Partial Features and Automatic Differentiation Correctness
From MaRDI portal
Publication:6414082
arXiv2210.08530MaRDI QIDQ6414082FDOQ6414082
Authors: Fernando Lucatelli Nunes, Matthijs Vákár 
Publication date: 16 October 2022
Abstract: We 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.
Theory of programming languages (68N15) Symbolic computation and algebraic computation (68W30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Functor categories, comma categories (18A25) Enriched categories (over closed or monoidal categories) (18D20)
This page was built for publication: Logical Relations for Partial Features and Automatic Differentiation Correctness
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6414082)
