Rencontre, 13 mars 2020

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 first-order straight-line programs, the rise of so-called differentiable programming in recent years has urged for the need of applying AD to complex programs, endowed with control flow operators and higher-order 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 simply-typed lambda-calculus, 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.

Lambda-calculi 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 leftmost-outermost reductions, and two less classic ones, non-deterministic weak call-by-value and least-level reductions.

Moreover, we present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by Hindley-Rosen 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 lambda-calculus, 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 lambda-calculus, among which de' Liguoro and Piperno's non-deterministic lambda-calculus and --for call-by-value-- 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 Identity-free Kleene Lattices

We provide a finite set of axioms for identity-free 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 Kleene-like algorithm.

We provide a finite set of axioms for identity-free 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 Kleene-like algorithm.