### 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.