BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:7596@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20170323T110000
DTEND;TZID=Europe/Paris:20170323T120000
DTSTAMP:20241120T204419Z
URL:https://www.i2m.univ-amu.fr/evenements/the-complete-unsoundness-of-coi
 nductive-intersection-types-and-how-to-escape-it/
SUMMARY:Pierre Vial (IRIF\, Université de Paris): The complete unsoundness
  of coinductive intersection types (and how to escape it)
DESCRIPTION:Pierre Vial: Certain type assignment systems are known to guara
 ntee or characterize normalization. The grammar of the types they feature 
 is usually inductive. It is easy to see that\, when types are coinductivel
 y generated\, we obtain unsound type systems (meaning here that they are a
 ble to type some mute terms). Even more\, for most of those systems\, it i
 s not difficult to find an argument proving that every term is typable (co
 mplete unsoundness). However\, this argument does not hold for relevant in
 tersection type systems (ITS)\, that are more restrictive because they for
 bid weakening. Thus\, the question remains: are relevant ITS featuring coi
 nductive types – despite being unsound – still able to characterize so
 me 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. Mor
 eover\, we prove that semantical information can be extracted from the typ
 ing derivations of D\, as the order of the typed terms. Our work also impl
 icitly provides a new non sensible relational model for pure λ-calculus.\
 n\nThe proofs cannot be handled directly with usual intersection operators
 \, so we introduce a new system that infinite sequences as intersection ty
 pes (System S). System S provides nice combinatorial features that allows 
 us to express the notion of typability of a term.\n\nEventually\, we expla
 in how soundness may be retrieved by means of a validity criterion that we
  call approximability. We then give an type-theoretical characterization o
 f 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 Normalizin
 g terms).\n\nhttp://www.irif.fr/~pvial/
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Pierre_Vial.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20161030T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR