Higher Order Automatic Differentiation of Higher Order Functions

We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher order language with algebraic data types, and we characterise it as the unique structure preserving macro given a choice of derivatives for basic operations. We describe a rich...

Full description

Bibliographic Details
Published in:	Logical Methods in Computer Science
Main Authors:	Mathieu Huot, Sam Staton, Matthijs Vákár
Format:	Article
Language:	English
Published:	Logical Methods in Computer Science e.V. 2022-03-01
Subjects:	computer science - programming languages computer science - logic in computer science
Online Access:	https://lmcs.episciences.org/7106/pdf

Similar Items

Higher-Order Asynchronous Effects
by: Danel Ahman, et al.
Published: (2024-09-01)

Modular coinduction up-to for higher-order languages via first-order transition systems
by: Jean-Marie Madiot, et al.
Published: (2021-09-01)

On the Termination Problem for Probabilistic Higher-Order Recursive Programs
by: Naoki Kobayashi, et al.
Published: (2020-10-01)

Theory of higher order interpretations and application to Basic Feasible Functions
by: Emmanuel Hainry, et al.
Published: (2020-12-01)

Cartesian closed 2-categories and permutation equivalence in higher-order rewriting
by: Tom Hirschowitz
Published: (2013-09-01)

On Higher-Order Probabilistic Subrecursion
by: Flavien Breuvart, et al.
Published: (2021-12-01)

Efficient Full Higher-Order Unification
by: Petar Vukmirović, et al.
Published: (2021-12-01)

SAT-Inspired Higher-Order Eliminations
by: Jasmin Blanchette, et al.
Published: (2023-05-01)

A Probabilistic Higher-order Fixpoint Logic
by: Yo Mitani, et al.
Published: (2021-12-01)

Convexity and Order in Probabilistic Call-by-Name FPC
by: Mathys Rennela
Published: (2020-11-01)

Extensional Semantics for Higher-Order Logic Programs with Negation
by: Panos Rondogiannis, et al.
Published: (2018-06-01)

Using higher-order contracts to model session types
by: Giovanni Bernardi, et al.
Published: (2016-06-01)

From nominal to higher-order rewriting and back again
by: Jesús Domínguez, et al.
Published: (2015-12-01)

A unifying framework for continuity and complexity in higher types
by: Thomas Powell
Published: (2020-09-01)

Complexity Hierarchies and Higher-order Cons-free Term Rewriting
by: Cynthia Kop, et al.
Published: (2017-08-01)

Decidability of higher-order matching
by: Colin Stirling
Published: (2009-07-01)

A categorical framework for congruence of applicative bisimilarity in higher-order languages
by: Tom Hirschowitz, et al.
Published: (2022-09-01)

Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
by: Guillaume Burel
Published: (2011-03-01)

Complete and tractable machine-independent characterizations of second-order polytime
by: Emmanuel Hainry, et al.
Published: (2025-01-01)

Contextual equivalence for higher-order pi-calculus revisited
by: Alan Jeffrey, et al.
Published: (2005-04-01)

Making first order linear logic a generating grammar
by: Sergey Slavnov
Published: (2023-11-01)

Relational $\star$-Liftings for Differential Privacy
by: Gilles Barthe, et al.
Published: (2019-12-01)

Isomorphisms of types in the presence of higher-order references (extended version)
by: Pierre Clairambault
Published: (2012-08-01)

Semantics of Higher-Order Recursion Schemes
by: Jiri Adamek, et al.
Published: (2011-04-01)

Logical Reasoning for Higher-Order Functions with Local State
by: Nobuko Yoshida, et al.
Published: (2008-10-01)

A tier-based typed programming language characterizing Feasible Functionals
by: Emmanuel Hainry, et al.
Published: (2022-02-01)

Monadic second-order definable graph orderings
by: Achim Blumensath, et al.
Published: (2014-01-01)

Superposition for Lambda-Free Higher-Order Logic
by: Alexander Bentkamp, et al.
Published: (2021-04-01)

A Functional (Monadic) Second-Order Theory of Infinite Trees
by: Anupam Das, et al.
Published: (2020-10-01)

Polynomial Path Orders
by: Martin Avanzini, et al.
Published: (2013-11-01)

The computability path ordering
by: Frédéric Blanqui, et al.
Published: (2015-10-01)

Partially Ordered Automata and Piecewise Testability
by: Tomáš Masopust, et al.
Published: (2021-05-01)

Existential Definability over the Subword Ordering
by: Pascal Baumann, et al.
Published: (2023-12-01)

Positive First-order Logic on Words and Graphs
by: Denis Kuperberg
Published: (2023-07-01)

Moss' logic for ordered coalgebras
by: Marta Bílková, et al.
Published: (2022-08-01)

Order-Invariant Types and Their Applications
by: Pablo Barcelo, et al.
Published: (2016-04-01)

Monadic Second Order Logic with Measure and Category Quantifiers
by: Matteo Mio, et al.
Published: (2018-04-01)

Separating Regular Languages with First-Order Logic
by: Thomas Place, et al.
Published: (2016-03-01)

Defining Recursive Predicates in Graph Orders
by: Ramanathan S. Thinniyam
Published: (2018-09-01)

Partial Order Infinitary Term Rewriting
by: Patrick Bahr
Published: (2014-06-01)