5 citations · 8 across the 6 of their papers we have counts for
6 papers
Simply Typed Reverse-Mode Automatic Differentiation with Variants: Denotational Correctness via Idempotent Completion
Fernando Lucatelli Nunes, Diogo Simm, Matthijs Vákár
Reverse-mode automatic differentiation is commonly given a denotational account in which each source type has a single cotangent type. Variant types obstruct this simply typed repr…
Backpropagation for Effectful Languages I: Finite Probability and Discrete Output Algebraic Effects
Diogo Simm, Fernando Lucatelli Nunes, Matthijs Vákár
We analyse reverse-mode automatic differentiation (AD) for discrete probabilistic programs. Our construction is formulated in the framework of Combinatory Homomorphic Automatic Dif…
Unraveling the iterative CHAD
Fernando Lucatelli Nunes, Gordon Plotkin, Matthijs Vákár
Combinatory Homomorphic Automatic Differentiation (CHAD) was originally formulated as a semantics-driven source-to-source transformation for reverse-mode automatic differentiation…
Efficient CHAD
Tom Smeding, Matthijs Vákár
We show how the basic Combinatory Homomorphic Automatic Differentiation (CHAD) algorithm can be optimised, using well-known methods, to yield a simple, composable, and generally ap…
Logical Relations for Partial Features and Automatic Differentiation Correctness
Fernando Lucatelli Nunes, Matthijs Vákár
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 catego…
Automatic Differentiation for ML-family languages: correctness via logical relations
Fernando Lucatelli Nunes, Matthijs Vákár
We give a simple, direct and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by wo…