dc.contributor.author | Lucatelli Nunes, Fernando | |
dc.contributor.author | Vákár, Matthijs | |
dc.date.accessioned | 2023-06-19T13:49:24Z | |
dc.date.available | 2023-06-19T13:49:24Z | |
dc.date.issued | 2023-06-19 | |
dc.identifier.uri | http://publications.mfo.de/handle/mfo/4046 | |
dc.description.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. | en_US |
dc.description.sponsorship | This project has received funding via NWO Veni grant number VI.Veni.202.124 as well as the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No. 895827.
This research was supported through the programme “Oberwolfach Leibniz Fellows” by the Mathematisches Forschungsinstitut Oberwolfach in 2022. It was also partially supported by the CMUC, Centre for Mathematics of the University of Coimbra - UIDB/00324/2020, funded by the Portuguese Government through FCT/MCTES. | |
dc.language.iso | en | en_US |
dc.publisher | Mathematisches Forschungsinstitut Oberwolfach | en_US |
dc.relation.ispartofseries | Oberwolfach Preprints;2023-09 | |
dc.subject | Recursive Types | en_US |
dc.subject | Logical Relations | en_US |
dc.subject | Automatic differentiation | en_US |
dc.subject | Programming Languages | en_US |
dc.subject | Functional Programming | en_US |
dc.subject | Denotational Semantics | en_US |
dc.subject | Recursion | en_US |
dc.subject | Program Transformations | en_US |
dc.subject | Enriched Category Theory | en_US |
dc.title | Logical Relations for Partial Features and Automatic Differentiation Correctness | en_US |
dc.type | Preprint | en_US |
dc.rights.license | 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. | de |
dc.rights.license | 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. | en |
dc.identifier.doi | 10.14760/OWP-2023-09 | |
local.scientificprogram | OWLF 2022 | en_US |
local.series.id | OWP-2023-09 | en_US |
local.subject.msc | 68 | en_US |
local.subject.msc | 18 | en_US |
dc.identifier.urn | urn:nbn:de:101:1-2024032009190333483987 | |
dc.identifier.ppn | 1851823239 | |