Abstract FR:

L'interprétation abstraite et l'inférence de types sont deux méthodes formelles permettant d'obtenir de manière statique (i. E. à la compilation) et automatique une description approchée du comportement dynamique (i. E. De l'exécution) d'un programme. Ces deux méthodes sont généralement présentées comme concurrentes voir même incompatibles. Dans cet ouvrage, notre objectif a été tout d'abord de développer une approche générique permettant de définir un système de types en utilisant les techniques d'interprétation abstraite. Le résultat auquel nous sommes parvenus met ainsi fin à la polémique entre les tenants des techniques d'interprétation abstraite et ceux de l'inférence de types et ouvrent de nouveaux horizons pour aux techniques d'inférences. Il est désormais possible de combiner les techniques propres aux systèmes d'inférences de types et les techniques d'interprétation abstraite afin d'améliorer les systèmes de types existant, de développer de nouveaux systèmes de types. En résumé, notre objectif a été tout d'abord de développer dans cet ouvrage une approche générique permettant de définir un système de types en utilisant les techniques de l'interprétation abstraite, tout en exhibant les similitudes des systèmes obtenus avec les systèmes de types définis de manière classique. Ce formalisme une fois défini, nous illustrons comment utiliser les techniques spécifiques de l'interprétation abstraite afin d'améliorer de façon significative les systèmes de types classiques. Enfin, dans une dernière partie, nous définissons de nouveaux systèmes moins intuitifs permettant des typages bien plus précis que ceux disponibles dans la littérature