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:http://www.i2m.univ-amu.fr/spip.php?page=article&id_article=0
BEGIN:VEVENT
SUMMARY:Pierre VIAL - Representing permutations without permutations\, or the expressive power of sequence types
UID:20180319T101731-a123-e2286@https://www.i2m.univ-amu.fr
DTSTAMP:20180319T101731
DTSTART:20180607T110000
DTEND:20180607T123000
CREATED:20180319T101731
ATTENDEE;CN=Pierre VIAL:mailto:no-reply@math.cnrs.fr
LAST-MODIFIED:20180524T102416
LOCATION:Salle des séminaires 304-306 (3ème étage)
DESCRIPTION:An intersection type system with given features (strict or not\, idempotent or not\, relevant or not\, rigid or not...) characterizing\, e.g.\, a notion of normalization can be presented in various ways. Recent works by Asada\, Ong and Tsukada have championed a rigid description of resources. Whereas in non-rigid paradigms (e.g.\, standard Taylor expansion or non-idempotent intersection types)\, bags of resources are multisets and invariant under permutation\, in the rigid ones\, permutations must be processed explicitly and can be allowed or disallowed. Rigidity 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 set of integers. However\, one may wonder in what extent the absence of permutations causes a loss of expressivity w.r.t. reduction paths\, compared to a usual multiset framework or a rigid one with permutations. Our main contribution is to prove that not only every non-idempotent derivation can be represented by a rigid\, permutation-free derivation\, but also that any dynamic behavior may be captured in this way. In other words\, we prove that system S (sequential intersection) has full expressive power over multiset/ permutation-inclusive intersection. We do so in the most general setting\, i.e. by considering coinductive type grammars\, so that this work also applies in the study of the infinitary relational model. http://www.irif.fr/~pvial/ Pierre VIAL [
CATEGORIES:(Séminaire Logique et Interactions|textebrut|filtrer_ical)]
URL:http://www.i2m.univ-amu.fr/Seminaire-Logique-et-Interactions?id_evenement=2286
SEQUENCE:2
STATUS:CONFIRMED
END:VEVENT