Vendredi 22 Septembre

Retour à la vue des calendrier
Vendredi 22 Septembre
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Circular Proofs for Subtyping and Termination
Description: Rodolphe Lepigre In a recent (submitted) work with Christophe Raffalli, we designed a rich type
system for an extension of System F with subtyping. It includes primitive sums
and products, existential types, and (co-)inductive types. Using a combination
of (pointed) subtyping and circular proofs, we were able to express the system
with typing and subtyping rules that are syntax-directed (up to circularity).
During my talk, I will try to give you a flavour of the techniques we used. In
particular, I will show how choice operators can be used to get rid of typing
contexts, and to allow the commutation of quantifiers with other connectives.
I will then introduce the circular proof framework that is used for handling
inductive and co-inductive types in subtyping rules, and general recursion in
typing rules.