Séminaire, 1 décembre 2016
The meeting will take place
. in the morning, in room B1 (4th floor, Monod site, ENS de Lyon)
. in the afternoon, in amphi B (3rd floor, Monod site, ENS de Lyon)
Programme

Andrej Dudenhefner (Univ. Dortmund)Invited talk: Intersection Type Calculi of Bounded Dimension
In the realm of intersection type calculi exist several approaches to restrict or bound the rule of intersection introduction. The most prominent example are nonidempotent intersection types, where types are treated as a linear resource in order to allow for decidable inhabitation. We present a different restriction of the standard intersection type system based on a notion of dimension. Dimension intuitively measures intersection introduction (opposed to intersection types themselves) as a resource via proof theoretic decorations necessary for typing the term at its type. As a result, we have a nonidempotent and nonlinear interpretation of intersection that enjoys EXPSPACEcomplete inhabitation, vastly generalizing the rank2 result. Additionally, the induced dimensional analysis of (untyped) lambda calculus lends itself to inspect dimensionality of e.g. normal forms or terms typable in System F.

Tom Hirschowitz (HDR, Univ. Savoie)Invited talk: Shapely monads and analytic functors
In this work, we give precise mathematical form to the idea of a structure whose data and axioms are faithfully represented by a graphical calculus; some prominent examples are operads, polycategories, properads, and PROPs. Building on the established presentation of such structures as algebras for monads on presheaf categories, we describe a characteristic property of the associated monads — the shapeliness of the title — which says that ‘any two operations of the same shape agree’. In fact, shapeliness also gives a way to define the data and axioms of a structure directly from its graphical calculus, by generating a free shapely monad on the basic operations of the calculus.
This is joint with Richard Garner.

Pierre Vial (Université Paris 13)Invited talk: Some Uses of Infinitary Sequential Intersection
In this talk, we present an original coinductive type system, that we call S (S standing for "Sequence"). This system features intersection types that are sequence of types, instead of sets or multisets of types as in other framework. We develop a few applications of this type System.
A new answer to Klop's Question: in the early 90, Klop asked whether the set of hereditary headnormalizable terms could be characterized by type assignments. Tatsuta [07] showed that this was not possible with inductive type systems. We prove here that System S can answer positively to Klop's Question, provided we endow it with a validity condition (meant to discard some unsound proofs) that we call approximability.
A semantic for pure lambdacalculus: if we forget about the aforementioned validity criterion, we show that every term is typable in system S. Collapsing sequences on multisets, this provides a new model for pure lambdacalculus that does not equate all the non terminating terms (such a model is called nonsensible). One of the important feature of this model is that is gives a nonempty denotation to every term, including the most irregular ones (the socalled mute terms), and is able to discriminate terms according to their order (the number of abstractions that may prefix a term).
The surjectivity of the collapse of S on R: we show that every derivation of the infinitary version of Gardner/de Carvalho's System R (featuring multiset intersection) is the collapse of a derivation of S.