Pour le prochain séminaire de l’équipe Cosynus, nous aurons le plaisir d’accueillir Marie Kerjean pour son exposé intitulé Typing differentiable programming.

Résumé: Differentiable programming is a recent research area: its objective is to express differentiation as a modular algorithmic transformation on rich programming languages. It is in particular motivated by the various applications of automatic differentiation in machine learning or formal calculus. In this talk I will present joint work with Pierre-Marie Pédrot, focusing on the typing system used to express differentiation.

We will first review a few examples of differentiable languages recently exhibited in the literature. This allows to identity the linear Dialectica transformation as a reverse automated differentiation transformation on a higher-order lambda-calculus with positive types. Building on the intuitions provided by Dialectica and distribution theory, we construct a lambda-calculus with an internal differentiation operator. This calculus is typed by a type system inspired by Differential Linear Logic. Noticeably, we are able to express backward automatic differentiation as a call-by-name strategy and forward automatic differentiation as a call-by-value strategy.