Une approche calculatoire pour la conception de vérificateurs de types

Cet article présente une approche calculatoire pour la conception de vérificateurs de types, en les dérivant de spécifications comportementales à l'aide de raisonnements équationnels. Les auteurs simplifient les calculs en utilisant une approche algébrique basée sur la fusion de pliage et l'améliorent encore davantage avec une approche basée sur les contraintes pour résoudre et composer les préconditions de fusion. La méthodologie est illustrée par trois exemples de complexité croissante : un langage d'expression simple, un langage avec exceptions et une version du calcul lambda.