Typage modulaire des multi-méthodes
Institution:
Paris, ENMPDisciplines:
Directors:
Abstract EN:
This thesis presents a modular type system for languages with multi-methods, compatible with a core language a la ML with subtyping and type interference for the core language. Our presentation is modular as well, by defining an algebric type system that includes a core langage with fully abstract types. A language can be built by chosing constants and a language of types with an ordering. We identify conditions that guarantee the resulting language is statically safe. This presentation makes it possible to study more easily extensions in two directions while sharing a part of the safety proof : the formalization of our multi-methods as constants of the core language and the extension of the ML-Sub type system with kinding constraints to express modularly the type of « partially polymorphic » methods. Finally, we study the classical challenge of the « expression problem ». We also give an overview of the implementation of all those ideas in a complete language, Nice.
Abstract FR:
Cette thèse présente un système de types modulaire pour les langages à multi-méthodes, compatibles avec un noyau à la ML avec sous)-typage et inférence pour le langage noyau. Notre présentation est elle aussi modulaire, en posant un système de types algébriques comprenant un langage noyau avec des types entièrement abstraits. Un langage peut être construit par choix des constantes et du langage de types. Nous identifions les conditions sous lesquelles ce langage est statistiquement sûr. Cela facilite l’étude d’extensions dans deux directions, tout en partageant une partie de la preuve de sûreté : la formalisation des multi-méthodes comme des constantes du langage et un raffinement du système de types ML-Sub avec contraintes de kinding pour exprimer le type de méthodes « partiellement polymorphes ». Enfin, nous étudions le défi classique d « problème des expressions ». Nous donnons également un aperçu de la mise en œuvre de l’ensemble de ces idées dans un langage complet, Nice.