Pierre Vial (Université Paris 13), 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.