Reverse AD at higher types: pure, principled and denotationally correct

DOI10.1007/978-3-030-72019-3_22zbMath1473.68058arXiv2007.05283OpenAlexW3148154580MaRDI QIDQ2233481

Matthijs Vákár

Publication date: 18 October 2021

Full work available at URL: https://arxiv.org/abs/2007.05283

zbMATH Keywords

automatic differentiationsemanticsprogram correctness

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65) Numerical differentiation (65D25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

CHAD for expressive total languages ⋮ Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library ⋮ Unnamed Item ⋮ Reverse AD at higher types: pure, principled and denotationally correct

Cites Work

• Nesting forward-mode AD in a functional framework
• A linear logical framework
• Correctness of automatic differentiation via diffeologies and categorical gluing
• Reverse AD at higher types: pure, principled and denotationally correct
• A Categorical Semantics for Linear Logical Frameworks
• Quasitoposes, Quasiadhesive Categories and Artin Glueing
• Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
• Enriching an Effect Calculus with Linear Types
• Categorical combinators
• An introduction to differential linear logic: proof-nets, models and antiderivatives
• On the Versatility of Open Logical Relations
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Reverse AD at higher types: pure, principled and denotationally correct