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:7704@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20161117T110000
DTEND;TZID=Europe/Paris:20161117T120000
DTSTAMP:20241120T204805Z
URL:https://www.i2m.univ-amu.fr/evenements/practical-subtyping-for-system-
 f/
SUMMARY:Christophe Raffalli (LAMA\, Université de Savoie): Practical Subty
 ping for System F
DESCRIPTION:Christophe Raffalli: We present a rich type system with subtypi
 ng for an extension of System F. Our type constructors include sum and pro
 duct types\, universal and existential quantifiers\, inductive and coinduc
 tive types. Inductive and coinductive types may carry size annotations all
 owing the preservation of size invariants. For example it is possible to d
 erive the termination of the quick sort by showing that partitioning a lis
 t does not increase its size. The system is able to deal with complex prog
 rams involving mixed induction and coinduction\, or even mixed (co-)induct
 ion and polymorphism (as for Scott-encoded datatypes). One of the key idea
 s is the use of symbolic witnesses to handle quantifiers of all sorts. To 
 demonstrate the practicality of our system\, we provide an implementation 
 that accepts all the examples discussed in the paper and more.\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Christophe_Raffalli.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