Séminaire, 1 décembre 2016

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 non-idempotent 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 non-idempotent and non-linear interpretation of intersection that enjoys EXPSPACE-complete inhabitation, vastly generalizing the rank-2 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.

  • slides
• 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 head-normalizable 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 lambda-calculus: 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 lambda-calculus that does not equate all the non terminating terms (such a model is called non-sensible). One of the important feature of this model is that is gives a non-empty denotation to every term, including the most irregular ones (the so-called 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.