Séminaire, Jan. 14, 2016
The talks will take place
in salle des thèses (ground floor) in the morning;
in amphi I (not C !!!!  neither C, nor L) (ground floor, opposite part of the building) in the afternoon.
Programme
 10:30 – 12:00

Sam Staton (Oxford University)
 14:00 – 15:00

Raphaëlle Crubillé (Univ. Paris 7 & Univ. Bologna)Invited talk: Metrics Reasoning about lambdaterms
Terms of Church's lambdacalculus can be considered equivalent along many different definitions, but context equivalence is certainly the most direct and universally accepted one. However, this definition has the drawback of being based on an universal quantification over all contexts. In order to give handier characterisations, coinductive methodologies have been developped since 1990 by Abramsky (among others) for deterministic computations, and later by Lassen for nondeterministic ones, with new and exciting results appearing recently also for probabilistic languages: applicative bisimilarity, a coinductively defined notion of equivalence for functional programs, has been shown to be sound, and sometime even fully abstract, for probabilistic lambdacalculi. In the probabilistic case, however, equivalence can be seen as too discriminating: terms which have totally unrelated behaviours are treated the same as terms which behave very similarly. We study the problem of evaluating the distance between lambdaterms. A natural generalisation of context equivalence, is shown to be characterised in a restricted affine setting by a notion of trace distance, and to be bounded from above by a coinductively defined distance based on the Kantorovich metric on distributions. A different, again fullyabstract, tuplebased notion of trace distance is shown to be able to handle nontrivial examples, and to allow a generalisation to the nonaffine case.
 15:30 – 16:30

Lionel Vaux (Univ. AixMarseille)Invited talk: A characterization of strong normalizability as a finiteness structure via the Taylor expansion of λterms, with applications.
In the folklore of differential linear logic and its denotational models, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cutelimination.
We make this intuition formal in the context of λcalculus by introducing a finiteness structure on resource λterms, which is such that a λterm is strongly normalizing iff the support of its Taylor expansion is finitary.
This structure is a refinement of the one introduced by Ehrhard in his LICS 2010 paper: for the latter, we also prove that any strongly normalizing λterm has a finitary Taylor expansion (this was already known for the terms of system F), but the converse does not hold. As was already the case in Ehrhard's work, the proofs do not rely on any uniformity property, hence this approach is valid for nondeterministic extensions of the λcalculus as well.
One application of this work is the existence of a normal form for the Taylor expansion of any strongly normalizable term. We will moreover give a brief overview of our work in progress, allowing to extend our results to (must) normalizability and (must) head normalizability : this is the next step in a line of work aiming at a generalization of results by Ehrhard and Regnier [TCS vol. 403, 2008; CiE 2006] that were previously limited to a uniform setting.
(Joint work with Michele Pagani and Christine Tasson.)
To find amphi C, here is a not so clever route:
 go to amphi B (this you know), and find out that it's the wrong place;
 walk straight along the corridor where amphi B is, until you meet an elevator on your left: take it to the ground floor;
 exit the elevator, turn right, and then left after a few steps (that is, go inside the building instead of leaving it);
 go straight until you cannot anymore, follow the "Chocola" signs.