Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

DOI10.46298/lmcs-19(4:5)2023arXiv2112.07292MaRDI QIDQ6178671

François Pottier, Paulo Emílio de Vilhena

Publication date: 16 January 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

automatic differentiationseparation logicprogram verificationeffect handlers

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programming with algebraic effects and handlers
• Modular verification of programs with effects and effects handlers
• Modular verification of programs with effects and effect handlers in Coq
• Correctness of automatic differentiation via diffeologies and categorical gluing
• Reverse AD at higher types: pure, principled and denotationally correct
• Beautiful differentiation
• Evaluating Derivatives
• Handlers of Algebraic Effects
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Exception Handling in CLU
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic
• Typed Tagless Final Interpreters
• On the Versatility of Open Logical Relations
• Effect handlers via generalised continuations
• Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
• Functional differentiation of computer programs
• Separation Logic Tutorial
• Functional differentiation of computer programs
• An introduction to algebraic effects and handlers (invited tutorial paper)
• Shallow effect handlers

This page was built for publication: Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library