Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                          Lundi 30 septembre, 10h30

                              -----------------
                              Yann Régis-Gianas
                              -----------------

                           Université Paris Diderot

             ====================================================
             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.