Bric-à-brac
 |  |
| english | [french] |
Mon travail de recherche se situe dans le domaine du typage des langages de programmation. Cette technique permet d'analyser un programme de manière statique (c'est-à-dire sans l'exécuter) dans le but d'établir quelque propriété relative à son exécution. L'exemple le plus courant est l'absence d'erreurs à l'exécution, mais d'autres, comme des propriétés de sécurité, peuvent être considérées. En quelques mots, le typage consiste à associer à chaque fragment d'un programme un type qui décrit certains aspects de son comportement, et peut être déduit des types de ses sous-fragments par un ensemble de règles logiques. La détermination du type de chaque composant d'un programme peut être effectuée de manière manuelle par le programmeur en annotant le code source (dans ce cas, le système n'a qu'à vérifier la validité des types fournis), ou automatiquement, grâce à un algorithme d'inférence de types.
L'analyse de flots d'information consiste à déterminer de manière statique comment les sorties d'un programme sont reliées à ses entrées, i.e. comment les premières dépendent, de manière directe ou indirecte, des dernières. Cela permet en particulier de vérifier qu'un programme préserve le secret ou l'intégrité des données auquel il accède, c'est-à-dire montrer que certains aspects de son comportement ne donnent pas d'information sur ses entrées ``secrètes'', ou restent indépendantes de celles considérées ``non sûres''. Ces propriétés sont des instances de la non-interférence: elles expriment une certaine absence de dépendance.
J'ai conçu, avec François Pottier, une analyse de flots d'information pour le langage ML: un lambda-calcul en appel par valeur équipé de structures de données, de références et d'exceptions. Il s'agit du premier système de types pour l'analyse de flots d'information dans un langage de programmation réaliste dont la correction ait été prouvée: le calcul que nous avons étudié est en effet très proche du noyau du langage de programmation fonctionnel Caml. Un autre intérêt de ce travail réside dans le fait que, suivant la tradition de ML, notre système de type est équipé de polymorphisme et d'inférence. En plus de la structure des valeurs, nos types décrivent les flots d'information; le polymorphisme permet d'écrire du code générique vis-à-vis des deux. L'inférence de types est indispensable car les types des systèmes pour les flots d'information sont verbeux, et parce que les flots d'information sont souvent difficiles à analyser manuellement.
Enfin, j'ai implémenté le système Flow Caml: il s'agit d'une extension du compilateur Objective Caml avec le système de types précédent. Cela permet de confronter notre proposition à des cas réels et de tester sa viabilité. Un autre intérêt de Flow Caml réside dans le fait qu'il s'agit d'une des premières implantations d'un langage de programmation réaliste équipé de sous-typage et de polymorphisme.
Durant les dernières années, plusieurs chercheurs ont proposé des formulations de systèmes de type et d'algorithme d'inférence à base de contraintes, c'est-à-dire des assertions logiques portant sur les types et les variables de type. L'une des plus populaires est l'extension paramétrée du système ML, HM(X), dont la description originelle est due à Odersky, Sulzmann et Wehr. Comme cela est maintenant largement reconnu, l'introduction de contraintes est bénéfique pour au moins deux raisons. Premièrement, il est agréable de réduire l'inférence de type à la résolution de contraintes, même dans le cas simple de ML. Deuxièmement, cela permet de s'intéresser à des cadres plus généraux, comme les systèmes avec sous-typage.
Tout d'abord, j'ai étudié l'inférence de types dans les systèmes équipés de sous-typage structurel. Il s'agit d'une forme très répandue de sous-typage où deux types comparables doivent avoir la même forme et ne peuvent différer que par leurs feuilles atomiques (en particulier, il n'y a pas de plus petit ou plus grand type). Cette forme de sous-typage intervient naturellement lorsque l'on étend des systèmes de type à la ML avec des annotations atomiques appartement à un ensemble ordonné, dans le but d'effectuer une analyse statique (e.g. détection d'exceptions non rattrapées, analyse de flots de données ou d'information). J'ai en particulier proposé un algorithme réaliste et efficace de résolution de contraintes, pour l'inférence de types en présence de sous-typage structurel et de polymorphisme. La librairie Dalton est une implémentation de cette algorithme que j'ai réalisée en Objective Caml. Cette librairie vient comme un foncteur Caml paramétré par un ensemble de modules décrivant le système de types du client. Ainsi, j'espère qu'elle pourra être utilisé dans une variété d'applications. En particulier, je l'ai employée pour développer Flow Caml.
Je me suis également intéressé à plusieurs enrichissements du système HM(X). Tout d'abord, j'ai proposé une extension de HM(X) avec des data-types existentiels et universels bornés. Ce travail généralise l'extension de ML avec des types abstraits, d'Odersky et Läufer. L'inférence de type est ici réduite à la résolution de contraintes qui comprennent des formes (restreintes) de quantification universelle et d'implication. Ces constructions ne sont en général pas traitées par les solveurs existants pour le sous-typage. Cependant, j'ai également proposé un algorithme de résolution efficace pour le cas du sous-typage structurel.
Poursuivant ce travail, j'ai étudié, avec François Pottier, l'inférence de type pour les data-types algébriques gardés. Ces types, qui subsument les concepts connus dans la littérature sous les noms de types indexés, data-types récursifs gardés et types fantômes, et qui sont étroitement liés aux types inductifs, ont la caractéristique remarquable que, lors du typage d'une fonction définie par cas, chaque branche est vérifiée sous des hypothèses différentes. Ce mécanisme permet d'exploiter la présence de tests dynamiques dans le code pour produire des informations statiques. Ainsi, nous avons proposé une extension de HM(X) avec filtrage, data-types algébriques gardés et récursion polymorphe. Nous avons alors montré que, à l'aide de quelques annotations de types, la synthèse de type pour ce système peut être réduite à la résolution de contraintes.
| |
| english | [french] |