Any views expressed within media held on this service are those of the contributors, should not be taken as approved or endorsed by the University, and do not necessarily reflect the views of the University in respect of any particular issue.

【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

External link:

Passcode: 387885



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.


Report this page

To report inappropriate content on this page, please use the form below. Upon receiving your report, we will be in touch as per the Take Down Policy of the service.

Please note that personal data collected through this form is used and stored for the purposes of processing this report and communication with you.

If you are unable to report a concern about content via this form please contact the Service Owner.

Please enter an email address you wish to be contacted on. Please describe the unacceptable content in sufficient detail to allow us to locate it, and why you consider it to be unacceptable.
By submitting this report, you accept that it is accurate and that fraudulent or nuisance complaints may result in action by the University.