abstract 20/06/2002

20/06/2002: Vincent Balat (PPS)
Normalisation par �valuation en CAML avec type somme

Résumé Les langages fonctionnels comme CAML compilent les programmes en forme normale de t�te faible. La normalisation par �valuation est une technique permettant de tirer partie de l'�valuation dans un tel langage pour obtenir la forme normale forte de lambda-termes sous forme syntaxique. Cette technique a �t� utilis�e pour obtenir un algorithme d'�valuation partielle tr�s simple (type-directed partial evaluation).
Dans cet expos�, je pr�senterai les algorithmes de normalisation par �valuation et d'�valuation partielle dirig�e par les types, et j'en montrerai une impl�mentation en Objective Caml utilisant des op�rateurs de contr�le (shift et cupto).
Je montrerai ensuite comment ce proc�d� a �t� utilis� dans la preuve d'un r�sultat th�orique sur les isomorphismes de types avec sommes, et comment cette application a conduit � une optimisation de l'algorithme d'�valuation partielle pour la gestion des types sommes, permettant de r�duire consid�rablement la taille du r�sultat produit dans certains cas.

20/06/2002: Vincent Balat (PPS) Normalisation par �valuation en CAML avec type somme

20/06/2002: Vincent Balat (PPS)
Normalisation par �valuation en CAML avec type somme