Séminaire, 14 novembre 2019

Programme

10:30 – 12:00

Yann Régis-Gianas (IRIF, Univ. Paris Diderot)

Invited talk: Towards certified incremental functional programming

Data constantly change. Google engineers make one commit every 2 seconds on the same git repository. On average, Twitter receives approximatively 6000 tweets per second. A self-driving car typically updates 100MB of its state each second.

How do we program software systems to handle these changes? When data is made of tiny flat records like tweets, and when data processing is made of only purely local algorithms like statistical operators, stream-based programming is most of the time the right approach.

What if the data is more structured, typically like a source code repository? Can we follow a similar dataflow approach? That is not clear. We believe that incremental functional programming could provide better tools for that kind of situations.

Incremental functional programming is about implementing change-centric software systems using first-class changes. From a base input and a change to this input, an incremental program computes a change of the base output. More formally, if f is a function of type A → B and if there is a type ∆A for changes over values of type A, and a type ∆B for changes over values of type B, an incrementalization D(f) of f is such that f x ⊕ D(f) x dx = f (x ⊕ dx) where ⊕ is the application of a change to a value and D(f ) has type A → ∆A → ∆B.

In this talk, we will explain why incremental functional programming is important but error-prone. We will describe our ongoing work to develop ∆Caml and ∆Coq, two tools that assist the incremental programmer in certifying incremental functional programs.

• slides

14:00 – 15:00

Marie Kerjean (INRIA Nantes)

Invited talk: Higher-Order Distributions for Differential Linear Logic

Is differentiation as it appears in computer science the same as the one from standard mathematics ? In particular, can differentiation in linear logic compute on traditional objects of mathematics ?

Succeeding in finding such a smooth interpretation of differential linear logic requires to overcome several issues: finding a good category of reflexive spaces and understanding how to handle higher-order objects in functional analysis.

The first problem can be solved by exploiting the fact that polarities naturally appear in the theory of topological vector spaces; in particular the categories of spaces of distributions and their dual will provide an adequate example. For the second, I will review several solutions providing definitions for higher-order distributions.

This talk is based mainly on works in collaboration with Jean-Simon Lemay.

• slides

15:30 – 16:30

Francesco Gavazzo (IMDEA Software Institute)

Invited talk: Differential Logical Relations

In this talk, we introduce differential logical relations, a new form of logical relation which, in the spirit of metric relations, assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between programs not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity of the compared programs.

After having introduced the notion of a program distance, we will review some of the main notions of program distance offered by the literature and highlight their strengths and weaknesses. We will then introduce differential logical relations, their main properties, and their relationship with the aforementioned notions of program distance. Finally, we will discuss extensions and improvements of the current theory of differential logical relations.

• slides