Vérification de l'équivalence du $\pi$-calcul dans HOL
Résumé
Dans ce rapport, on décrit une représentation purement définitionnelle du $\pi$-calcul dans le prouveur de théorèmes HOL. Les lois algébriques du $\pi$-calcul sont montrées comme étant des théorèmes dans la logique d'ordre supérieur. Ainsi, on obtient un outil correcte dans lequel on peut raisonner sur des applications utilisant le $\pi$-calcul comme outil de spécification. Comme application, on montre par induction la correction de la spécification de l'addition naturelle en $\pi$-calcul.