La formalisation dans un assistants de preuves de propriétés sur la sémantique et le typage des langages de programmations permet
Cependant le problème de la représentation des liaisons de variables rend cette tâche de formalisation délicate. Les approches traditionnelles (représentation nommée, indices de de Bruijn, syntaxe abstraite d'ordre supérieure, ...), bien que pouvant être adaptées pour certaines formalisations, ne fournissent pas une solution générale au problème.
Je présenterai une nouvelle méthode qui consiste à combiner une représentation "locally nameless" des termes (où les variables liés sont représentés par des indices de de Bruijn tandis que les variables libres sont nommées) avec une quantification cofinie des noms libres qui apparaissent dans les définitions inductives sur les termes. En suivant ce style, il n'y a pas besoin de raisonner sur l'alpha- conversion, ni sur l'équivariance (le fait que les noms libres peuvent être renommés dans les dérivations).
Bien que ces ingrédients sur lesquels on s'appuie aient été utilisés auparavant, la combinaison que l'on en fait ici est particulièrement intéressante : elle amène a des développements concis et, surtout, qui suivent fidèlement la structure des preuves "papier" correspondantes. Je vous donnerai aussi un petit aperçu des scripts Coq des preuves sur lesquelles j'ai travaillé (soundness de System-Fsub et de ML plus extensions, et préservation du typage pour le Calcul des Constructions).