Prochain séminaire/GdT :

Circular Proofs for Subtyping and Termination
Rodolphe Lepigre
Salle B107, bâtiment B, Université de Villetaneuse
22/09/2017 11:00 - 12:30
Résumé :

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.

Séminaires/GdT à venir (peut changer)

Séminaires/GdT passés