[The talk will take place in amphi A, 3rd & 4th floors, at the other end of the corridor w.r.t. amphi B, if you know where this is.]

Dialectica is a proof transformation acting of intuitionnistic logic which factors through Girard's translation, 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.

This is joint work with Pierre-Marie Pédrot.