Séminaire, 1 octobre 2015

Programme

10:30 – 12:00
Ugo de'Liguoro (Università di Torino)
Invited talk: Intersection types for lambda-calculi with control

We investigate lambda-calculi extended with control operators from the point of view of intersection type theories. Intersection types are a natural bridge between syntax and semantics and have been extensively used to characterize computational properties of the untyped lambda-calculus. We aim at extending these techniques and results to calculi with control, whose semantics is usually given either in terms of CPS translations or of abstract machines. Building over a denotational model of continuations due Streicher and Reus, that is a model of several such calculi (including Felleisen's lambda-C, Parigot's lambda-mu, De Groote and Saurin's Lambda-mu and Krivine's lambda/cc), and using Abramsky's ideas on domain logic, we show how type theories and type assignment systems can be obtained out of Streicher and Reus models as well as of the"extensional" variant by Nakazawa and Katsumata, all inducing filter models in the sense of Barendregt-Coppo-Dezani. We eventually mention some results about strongly normalizing terms of Parigot's lambda-mu and the approximation theorem for De Groote-Saurin's Lambda-mu.

14:00 – 15:00
Thomas Leventis (Institut de Mathématiques de Luminy)
Invited talk: Theories in Probabilistic lambda-calculus.

Our goal is to extend the notion of lambda-theory to the call-by-name probabilistic lambda-calculus. We will first describe this calculus without using probabilistic reductions nor specifying a reduction strategy, so that we can give a meaning to the notion of beta-equivalence. We will then define probabilistic lambda-theories, as well as the notions of extensionality and sensibility for such theories. Lastly we will present a result similar to the one proved by Martin Hyland in usual lambda-calculus: there is a maximum consistent extensional sensible lambda-theory, and it is given by the equality of Böhm trees or equivalently by the observational equivalence of terms.

15:30 – 16:30
Beniamino Accattoli (INRIA)
Invited talk: Proof nets and the lambda-calculus 2.0

The traditional proof nets representation of lambda-calculus dates back to the nineties, to the work of Danos and Regnier, and it is nowadays a cornerstone of the linear logic literature.

In the last few years such a traditional view has been refined, building on a simple solution to its main issue, i.e. the different granularities of the evaluation mechanisms at work in the two systems. Such a solution, the linear substitution calculus, is both a refinement of lambda calculus and a graph-free presentation of proof nets. Its simplicity led to a new wave of studies on the topic, whose main achievement has been the development of a theory of cost models for the lambda calculus.

The talk will be an introduction to the main ideas at work in the new framework, that are:

  1. an abstract point of view on proof nets, seen as a rewriting system up to a postponable structural equivalence, and not as a graphical language;

  2. a new, simpler presentation of linear head reduction, justified via rewriting and quantitative analyses;

  3. the extension of the theory to abstract machines and processes, them too seen as abstract proof nets evaluating via linear head reduction;

  4. the use of strong bisimulations to relate terms, graphs, machines, and processes in a perfect way.

Beware: the talk will not be a bland survey of previous work, nor will it present recent results, in particular not those about cost models. It will rather be an original introduction to basic concepts, questioning the status quo, and stressing the change of perspective.