|
|
 |
|
Mardi 5 Septembre
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
On the shape of random Pólya structures |
| Description: |
Michael Wallner |
Mardi 19 Septembre
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
TBA |
| Description: |
Valentin Bonzom |
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. |
|
|
