The complete unsoundness of coinductive intersection types (and how to escape it)

Pierre Vial
IRIF, Université de Paris

Date(s) : 23/03/2017   iCal
11 h 00 min - 12 h 00 min

Certain type assignment systems are known to guarantee or characterize normalization. The grammar of the types they feature is usually inductive. It is easy to see that, when types are coinductively generated, we obtain unsound type systems (meaning here that they are able to type some mute terms). Even more, for most of those systems, it is not difficult to find an argument proving that every term is typable (complete unsoundness). However, this argument does not hold for relevant intersection type systems (ITS), that are more restrictive because they forbid weakening. Thus, the question remains: are relevant ITS featuring coinductive types – despite being unsound – still able to characterize some bigger class of terms? We show that it is actually not the case: every term is typable in a standard relevant coinductive ITS that we call D. Moreover, we prove that semantical information can be extracted from the typing derivations of D, as the order of the typed terms. Our work also implicitly provides a new non sensible relational model for pure λ-calculus.

The proofs cannot be handled directly with usual intersection operators, so we introduce a new system that infinite sequences as intersection types (System S). System S provides nice combinatorial features that allows us to express the notion of typability of a term.

Eventually, we explain how soundness may be retrieved by means of a validity criterion that we call approximability. We then give an type-theoretical characterization of some class of infinitarily normalizing terms i.e. the set of terms whose Böhm tree does not hold bottom (the so called Hereditary Head Normalizing terms).


Retour en haut 

Secured By miniOrange