Towards a Formalization of pi-calculus Processes in Higher Order Abstract Syntax
Résumé
Higher order abstract syntax is a natural way to formalize programming languages with binders, like the pi-calculus, because alpha-conversion and beta-reduction are delegated to the meta level of the provers, making tedious substitutions superfluous. However, such formalizations usually lack induction principles, and often give rise to exotic terms. Induction is necessary in syntax analysis, and certain important syntactic properties might be invalid in the presence of exotic terms. The paper introduces well formedness predicates for the pi-calculus with which exotic terms are excluded and, simultaneously, induction principles are obtained. The principles are then used in formal proofs of vital syntactic properties, mechanized in Isabelle/HOL.
La syntaxe abstraite d'ordre supérieur est une technique pour la formalisation de langages comportant des constructions liantes tels que le pi-calcul. Grâce à cette technique, l'utilisateur n'a pas à gérer explicitement une notion de substitution, l'alpha-conversion et la béta-réduction faisant intervenir les variables du niveau meta; Cependant, dans une telle approche, l'on ne dispose pas de principe d'induction de manière naturelle, et de plus le langage tel qu'il est formalisé peut englober des termes considérés comme exotiques; Dans ce travail nous définissons des prédicats de bonne formation pour le pi-calcul permettant d’éliminer les termes exotiques et fournissant des principes d'induction? Ceci rend possible la preuve de propriétés syntaxiques essentielles pour le pi-calcul., que nous formalisons dans le système Isabelle/HOL
Origine : Fichiers produits par l'(les) auteur(s)