BEGIN:VCALENDAR
VERSION:2.0
X-WR-TIMEZONE:Europe/Paris
CALSCALE:GREGORIAN
PRODID:-//SPIP/Plugin Agenda//NONSGML v1.0//FR
X-WR-CALNAME;VALUE=TEXT: -- Institut de Mathématiques de Marseille\, UMR 7373
X-WR-RELCALID:https://www.i2m.univ-amu.fr/spip.php?page=article&id_article=0
BEGIN:VEVENT
SUMMARY:Pierre VIAL - The complete unsoundness of coinductive intersection types (and how to escape it)
UID:20170126T111246-a123-e1637@https://www.i2m.univ-amu.fr
DTSTAMP:20170126T111246
DTSTART:20170323T110000
DTEND:20170323T120000
CREATED:20170126T111246
ATTENDEE;CN=Pierre VIAL:mailto:no-reply@math.cnrs.fr
LAST-MODIFIED:20170322T113339
LOCATION:Salle des séminaires 304-306 (3ème étage)
DESCRIPTION: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). http://www.irif.fr/~pvial/[
CATEGORIES:(Séminaire Logique et Interactions|textebrut|filtrer_ical)]
URL:https://www.i2m.univ-amu.fr/Seminaire-Logique-et-Interactions?id_evenement=1637
SEQUENCE:1
STATUS:CONFIRMED
END:VEVENT