Séminaire, 14 janvier 2016

Programme

10:30 – 12:00

Sam Staton (Oxford University)

Invited talk: Algebraic effects, linearity, and quantum programming languages

14:00 – 15:00

Raphaëlle Crubillé (Univ. Paris 7 & Univ. Bologna)

Invited talk: Metrics Reasoning about lambda-terms

Terms of Church's lambda-calculus 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 non-deterministic 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 lambda-calculi. 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 lambda-terms. 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 fully-abstract, tuple-based notion of trace distance is shown to be able to handle nontrivial examples, and to allow a generalisation to the non-affine case.

15:30 – 16:30

Lionel Vaux (Univ. Aix-Marseille)

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 cut-elimination.

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 non-deterministic 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.)

• slides