Por Marie Kerjean (LIPN - Université Paris 13).

Differential Linear Logic is an extension of Linear Logic allowing for the linearization of proofs. It was introduced by Ehrhard and Regnier 20 years ago. Its denotational models corresponds to the differentiation of higher-order functions in functional analysis, and it has led to differential extensions of lambda-calculus and categorical models of linear logic.

Dialectica is a proof transformation introduced by Gödel acting of intuitionistic 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.

Transmissão via Zoom.