Séminaire, 1 octobre 2015
Programme
 10:30 – 12:00

Ugo de'Liguoro (Università di Torino)Invited talk: Intersection types for lambdacalculi with control
We investigate lambdacalculi 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 lambdacalculus. 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 lambdaC, Parigot's lambdamu, De Groote and Saurin's Lambdamu 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 BarendregtCoppoDezani. We eventually mention some results about strongly normalizing terms of Parigot's lambdamu and the approximation theorem for De GrooteSaurin's Lambdamu.
 14:00 – 15:00

Thomas Leventis (Institut de Mathématiques de Luminy)Invited talk: Theories in Probabilistic lambdacalculus.
Our goal is to extend the notion of lambdatheory to the callbyname probabilistic lambdacalculus. 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 betaequivalence. We will then define probabilistic lambdatheories, 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 lambdacalculus: there is a maximum consistent extensional sensible lambdatheory, 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 lambdacalculus 2.0
The traditional proof nets representation of lambdacalculus 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 graphfree 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:
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;
a new, simpler presentation of linear head reduction, justified via rewriting and quantitative analyses;
the extension of the theory to abstract machines and processes, them too seen as abstract proof nets evaluating via linear head reduction;
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.