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: 4^th floor Bayes Centre

External link: https://meeting.huaweicloud.com/welink/webrtc/?lang=en-US#/j/95878720

Passcode: 387885

Abstract

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.

Bio

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.

【BAYES COFFEE HOUSE TECH TALK SERIES】The differentiation monad / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0