Algorithmes de vérification de type

Je commence une recherche bibliographique personnelle sur les algorithmes de vérification de type et souhaite quelques conseils. Quels sont les algorithmes, stratégies et techniques générales de vérification de type les plus couramment utilisés?

Je m'intéresse particulièrement aux algorithmes de vérification de type complexes qui ont été implémentés dans des langages typés fortement statiques largement connus tels que, par exemple, C ++, Java 5+, Scala ou autres. IE, algorithmes de vérification de type qui ne sont pas très simples en raison du typage très simple du langage sous-jacent (comme Java 1.4 et inférieur).

Je ne suis pas en soi intéressé par un langage spécifique X, Y ou Z. Je suis intéressé par les algorithmes de vérification de type quel que soit le langage qu'ils ciblent. Si vous fournissez une réponse comme "la langue L dont vous n'avez jamais entendu parler et qui est fortement typée et le typage est complexe a un algorithme de vérification de type qui fait A, B et C en vérifiant X et Y en utilisant l'algorithme Z", ou "le la stratégie X et Y utilisée pour Scala et une variante Z de A utilisée pour C # sont cool à cause des fonctionnalités R, S et T qui fonctionnent de cette façon ", alors les réponses sont bonnes.

La plupart des recherches ne publient pas réellement les algorithmes de vérification de type pour les langages de programmation complets. Vous trouverez quelques formalisations d'une grande partie des systèmes de types pour les langages de programmation complets, comme le travail effectué par Drossopoulou et Eisenbach pour Java ou le travail de Nipkov et al sur C ++ . Plus souvent, cependant, vous ne trouverez les systèmes de types que pour une partie essentielle du langage (Featherweight Java en est un exemple) ou pour les concepts de base d'un langage tels que l' approche d'inférence de type locale de scala .

Dans les conférences telles que POPL et ICFP, vous trouverez de nombreux algorithmes de vérification de type pour des types spécifiques de systèmes de type, et de nouvelles approches telles que la vérification de type bidirectionnelle et tridirectionnelle .

Plus généralement, vous devez probablement connaître l' algorithme Damas-Milner , l'inférence de type locale, la vérification de type bidirectionnelle et tridirectionnelle et développer à partir de là, en suivant les références dans les articles et en utilisant google scholar pour trouver les articles qui les citent et s'appuyer sur les approches décrites. En outre, comme suggéré ci-dessus, les conférences telles que POPL, ICPF, ESOP et même ECOOP et OOPSLA auront des documents pertinents pour votre quête.

Un outil de base est la grammaire des attributs . Vous ne serez peut-être pas en mesure de faire tout ce que vous pouvez imaginer de méchant avec eux, mais ils sont un bon point de départ.

Essentiellement, vous pouvez parcourir l'arborescence de syntaxe abstraite d'un programme de haut en bas et / ou de bas en haut et transmettre des informations. Ainsi, par exemple, vous pouvez transmettre des informations de type de portée globale (par exemple, les classes et leurs membres) vers le bas et déterminer le type d'expressions de manière récursive, c'est-à-dire de bas en haut, en passant les types résultants vers le haut.

Trouvez quelques explications et exemples dans les diapositives ici (chapitre 5).