∂ is for Dialectica

February 13, 2023

Marie Kerjean (LIPN, Université Sorbonne Paris Nord)

Dialectica is a proof transformation acting of intuitionnistic logic, allowing
the realization of several semi-classical axioms such as Markov’s principle. By
taking the viewpoint of differential lambda-calculus and recent developments in
differentiable programming, we will show how Dialectica computes higher-order
backward differentiation. We will illustrate this through the lens of
categories, types and lambda-terms.