Subject: Une analyse de l'interaction dans le système F-13/11/98-Rocquecourt-FR Jour: 13/11/98 (Vendredi 13 novembre) CHANGEMENT DE DATE http://pauillac.inria.fr/bin/calendar/Seminaires S E M I N A I R E ____ ____ ___ / _ _ / __ __ /_ _ / / | _ __ _ / / \ / \ ___ / / | / /_ / __| / ___ /___/ __| / | __| |___ |_/ |_/ |____ / / __/ |_ |_/ |_ / |_/ / |_/ / ------------------------------------------------------------------------------------ Ce seminaire remplace celui initialement programme le 6 novembre. ------------------------------------------------------------------------------------ I N R I A - Rocquencourt, Salle de confe'rence du batiment 11 Vendredi 13 novembre, 10h30 ------------------- Hugo Herbelin ------------------- Universite Paris 10 et Nanterre ============================================================ Une analyse de l'interaction dans le système F (et des conséquences) ============================================================ En raisonnant avec des termes éta-expansés, nous montrons que l'arité des termes du système F peut être conservée (disons plutôt contrôlée) même si au cours de la réduction, celle-ci est apparemment perdue par instantiation de type. Le truc pour cela est de retarder les instantiations de type et de se restreindre à une réduction de type "appel par nom" ou "appel par valeur" (c.-à.-d. une réduction effectuée dans une machine à environnement). De cette analyse, nous tirons quelques sous-produits. D'abord la possibilité d'obtenir une machine à environnement pour le système F (ou pour le système LF, ou tout simplement un calcul polymorphe à la ML) qui fonctionne par blocs d'arguments plutôt qu'argument par argument. Dans la variante "appel par valeur" de cette machine, on obtient une extension au cas polymorphe de la machine abstraite du langage Pascal (seule la pile est nécessaire au contrôle). Ensuite, une caractérisation en terme de jeux de la réduction dans le système F qui généralise celle du cas simplement typé par Coquand, Nickau, Hyland-Ong ou Abramsky-Jagadeesan-Malacaria. J'ai un temps cru que cette approche s'étendait directement au système Fw et au Calcul des Constructions (CC). En fait, l'extension s'avère beaucoup plus complexe et l'arité peut devenir incontrôlable. Nous nous contenterons d'esquisser ce que deviennent les termes et la réduction dans CC lorsque les arguments sont traités par bloc.