TypiCal

Intervenant : Barbara Petit (ENS Lyon)

Date et lieu : 11/06/09, salle de conférence du Lix

Résumé : Le lamba-calcul avec constructeurs, de Arbiser, Miquel et Rios est une extension du lambda calcul avec un mecanisme de filtrage. Le filtrage "a la ML" y est decomposé en deux opérations elementaires: une analyse de cas sur des constantes, et une regle de commutation -surprenante au premier abord- entre le case et l'application.
Apres avoir presenté ce calcul, je lui definirai un systeme de types polymorphe avec unions et intersections. Enfin je montrerai un modele de realisabilite (proche candidats de reductibilites de Girard) pour ce systeme, et les proprietes de normalisation forte et de sureté vis a vis du filtrage qui en decoulent.

Liens : http://perso.ens-lyon.fr/barbara.petit/recherche.php