4 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…
Free Doubly-Infinitary Distributive Categories are Cartesian Closed
Fernando Lucatelli Nunes, Matthijs Vákár
We study the composite free completion Dist(C) := Fam(Fam(C^op)^op), obtained by first freely adjoining small products and then freely adjoining small coproducts. A natural pseudod…