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:7298@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20180607T110000
DTEND;TZID=Europe/Paris:20180607T123000
DTSTAMP:20241120T203903Z
URL:https://www.i2m.univ-amu.fr/evenements/representing-permutations-witho
 ut-permutations-or-the-expressive-power-of-sequence-types/
SUMMARY:Pierre Vial (IRIF\, Université de Paris): Representing permutation
 s without permutations\, or the expressive power of sequence types
DESCRIPTION:Pierre Vial: An intersection type system with given features (s
 trict or not\, idempotent or not\, relevant or not\, rigid or not...) char
 acterizing\, e.g.\, a notion of normalization can be presented in various 
 ways. Recent works by Asada\, Ong and Tsukada have championed a rigid desc
 ription of resources. Whereas in non-rigid paradigms (e.g.\, standard Tayl
 or expansion or non-idempotent intersection types)\, bags of resources are
  multisets and invariant under permutation\, in the rigid ones\, permutati
 ons must be processed explicitly and can be allowed or disallowed. Rigidit
 y enables a fine-grained control of reduction paths and their effects on\,
  e.g.\, typing derivations. We previously introduced system S\, featuring 
 a sequential intersection: a sequence is a family of types indexed by a se
 t of integers. However\, one may wonder in what extent the absence of perm
 utations causes a loss of expressivity w.r.t. reduction paths\, compared t
 o a usual multiset framework or a rigid one with permutations. Our main co
 ntribution is to prove that not only every non-idempotent derivation can b
 e represented by a rigid\, permutation-free derivation\, but also that any
  dynamic behavior may be captured in this way. In other words\, we prove t
 hat system S (sequential intersection) has full expressive power over mult
 iset/ permutation-inclusive intersection. We do so in the most general set
 ting\, i.e. by considering coinductive type grammars\, so that this work a
 lso applies in the study of the infinitary relational model.\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:DAYLIGHT
DTSTART:20180325T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR