Les langages à objets offrent une forme particulière de polymorphisme en permettant l'écriture de « méthodes » dont l'exécution dépend du type dynamique des arguments. Ce « dispatch dynamique » ne prend généralement en compte qu'un argument unique. Certains langages permettent le dispatch simultané sur tous les arguments et on parle alors de « multi-méthodes ». Cette thèse s'intéresse à la définition et au typage d'un langage dérivant de ML avec multiméthodes. Celles-ci sont introduites comme un cas particulier de filtrage sur les objets. La présentation du système de types utilise une approche algébrique. Plutôt que de figer l'ensemble des types, on en axiomatise les propriétés nécessaires pour la correction du système. Cela permet d'écrire des preuves génériques qui ne dépendent pas du choix de l'algèbre. On montre ainsi comment réduire la vérification automatique du typage à la résolution de problèmes simples du premier ordre (contraintes). La résolution des problèmes de contraintes peut alors réutiliser le corpus de résultats disponibles dans la littérature. L'avantage de cette approche algébrique est qu'elle permet de traiter d'un coup toute une classe de langages possibles se distinguant par la nature de l'algèbre de types, du langage d'expression des contraintes et du modèle d'interprétation de ces contraintes. Elle offre également un outil intéressant pour étudier le typage dans un contexte où le monde d'interprétation est ouvert, c'est-à-dire quand on souhaite que le typage d'un module apporte une garantie pour toutes les utilisations possibles de ce module.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00007516 |
| Date | 18 June 2004 |
| Creators | Frey, Alexandre |
| Publisher | École Nationale Supérieure des Mines de Paris |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0103 seconds