Rencontre, March 13, 2020
[un vendredi!]
le matin : pause café devant l'amphi B (comme toujours), puis on va en amphi K ; l'aprèsmidi : amphi A
Programme
 10:30 – 12:00

Damiano Mazza (CNRS, Univ. Paris 13)Invited talk: Automatic Differentiation in PCF
Automatic differentiation (AD) is the science of efficiently computing the derivative (or gradient, or Jacobian) of functions specified by computer programs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for training deep neural networks. Albeit AD techniques natively focus on a restricted class of programs, namely firstorder straightline programs, the rise of socalled differentiable programming in recent years has urged for the need of applying AD to complex programs, endowed with control flow operators and higherorder combinators, such as map and fold. In this talk, I will discuss the extension of AD algorithms to PCF, a(n idealized) purely functional programming language. We will first consider the simplytyped lambdacalculus, showing in particular how linear negation is related to reverse mode AD (aka backpropagation), and then see how the extra features of PCF, namely full recursion and conditionals, may be dealt with, stressing the difficulties posed by the latter.
[Joint work with Aloïs Brunel (Deepomatic) and Michele Pagani (IRIF, Université de Paris)]
 14:00 – 15:00

Giulio Guerrieri (University of Bath (UK))Invited talk: Factorization, Normalization and all that.
Lambdacalculi come with no fixed evaluation strategy. Different strategies may then be considered, and it is important that they satisfy some abstract rewriting property, such as factorization or nomalization theorems. We provide simple proof techniques for these theorems. Our starting point is a revisitation of Takahashi's technique to prove factorization for head reduction. Our appraoch is both simpler and more powerful, as it works in cases where Takahishi's does not. We then pair factorization with two other abstract properties, defining essential systems, and show that normalization follows. Concretely, we apply the technique to four case studies, two classic ones, head and the leftmostoutermost reductions, and two less classic ones, nondeterministic weak callbyvalue and leastlevel reductions.
Moreover, we present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by HindleyRosen result for confluence. Our technique is first developed abstractly. In particular, we isolate a simple sufficient condition (called linear swap) for lifting factorization from components to the compound system. We then closely analyze some common factorization schemas for the lambdacalculus, and show that the technique simplifies even more, reducing to the test of elementary local commutations. Concretely, we apply our modular technique to various extensions of the lambdacalculus, among which de' Liguoro and Piperno's nondeterministic lambdacalculus and for callbyvalue Carraro and Guerrieri's shuffling calculus. For both calculi the literature contains factorization theorems. For each, we provide a novel, neat, and strikingly short modular proof.
This is joint work with Beniamino Accattoli and Claudia Faggian.
 15:30 – 16:30

Amina Doumane (CNRS, ENS de Lyon)Invited talk: Completeness for Identityfree Kleene Lattices
We provide a finite set of axioms for identityfree Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeteness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleenelike algorithm.
We provide a finite set of axioms for identityfree Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeteness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleenelike algorithm.