******************************************************************* * LIENS Ecole Normale Superieure * * Les vendredis de l'equipe * * 'Semantique et Interpretation Abstraite' * * P. Cousot * * Salle J-L Verdier, Passage Vert, 14h--16h * * DMI ENS 45 rue d'Ulm 75005 Paris * ******************************************************************* *** Vendredi 9 octobre 1992 *** Reunion de travail **************** B. Monsuez Higher-order strictness analysis by type inference. *** Vendredi 16 octobre 1992 *** Seminaire ************************ Une methode rapide de preuve automatique en logique classique du premier ordre. Jean Goubault (BULL) Resume: le theoreme de Herbrand, fondement des methodes completes de demonstration automatique actuelles comme la resolution ou la methode des connexions, est ici soumise a un reexamen. La preuve devient un probleme de jeux sur des graphes entre un planificateur et un unificateur, le but du planificateur etant de reduire la formule de depart a une tautologie, celui de l'unificateur etant de reduire la marge de manoeuvre du precedent. Une strategie de recherche de la preuve, fondee sur le principe de la minimisation du facteur de branchement dans l'arbre de recherche, est presentee. Les resultats, tant pratiques (benchmarks) que theoriques (nature et complexite des problemes de preuve), seront degages. Les analogies avec les methodes plus classiques seront esquissees. *** Vendredi 23 octobre 1992 *** Seminaire ************************ Type Inference by Abstract Interpretation Bruno Monsuez (LIENS) Resume: We presents a generic method which uses the framework of Abstract Interpretation as defined by the Cousots to build type reconstruction algorithms. Fundamentally, this method is based upon the combination of an upper and a lower approximation as well as the use of widening operators to insure algorithm termination. We illustrate this method with a type reconstruction algorithm of the expressions of a ML-like language more or less similar to ML+. We first show that restricting recursive constants to monomorphic types -- as in ML -- can be seen as a widening operator. Then we exhibit a less restrictive operator which lets recursive defined expressions have polymorphic types, while still insuring algorithm termination. *** Vendredi 30 octobre 1992 *** Relache ************************** *******************************************************************