【BAYES COFFEE HOUSE TECH TALK SERIES】The differentiation monad
Marie Kerjean will give a talk, in person and online, for the Coffee House Tech Talk Series. Details of the talk are below.
Title: The differentiation monad
Speaker: Marie Kerjean
When: 11am Tue 31 Oct
Where: 4th floor Bayes Centre
Differentiation in theoretical computer science has become increasingly popular since the rise of automatic differentiation in machine learning. Differentiable Programming is a recent field that explores modular, typed and principled ways to differentiate programs algorithmically.
Differentiation, however, was studied independently through linear logic, giving rise in particular to differential Linear logic. This first approach of differentiation is directly inspired by denotational models of Linear Logic. In particular, they take their source in quantitative semantics, where programs are interpreted as power series.
Quantitative semantics, in turn, has been influential in giving models to probabilistic programming and redefining approximations and proof methods in lambda calculus.
In this talk, we will approach differentiation from a monadic point of view. We will see how a twist in the continuation monad forces a quantitative setting in programming languages. We will see how this new monad comes from the search for a fourth missing rule in Differential Linear Logic. Finally, we will dive into concrete interpretations of this monad and put forward the link with graded monads. This is based on joint work with Jean-Simon Pacaud Lemay.
Marie Kerjean is a CNRS researcher at the LIPN Lab in Paris. She focuses on making links between functional analysis and logic: she’s an expert in differential linear logic and in the formalization of analysis within the Coq proof assistant. Before being a CNRS researcher, she was a post-doctoral student at INRIA.