Towards a Formalization of pi-calculus Processes in Higher Order Abstract Syntax - LARA - Libre accès aux rapports scientifiques et techniques Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2000

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
Fichier principal
Vignette du fichier
RR2000-23.pdf (393.84 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-02101817 , version 1 (17-04-2019)

Identifiants

  • HAL Id : hal-02101817 , version 1

Citer

Christine Roeckl, Daniel Hirschkoff, Stefan Berghofer. Towards a Formalization of pi-calculus Processes in Higher Order Abstract Syntax. [Research Report] LIP RR-2000-23, Laboratoire de l'informatique du parallélisme. 2000, 2+15p. ⟨hal-02101817⟩
29 Consultations
71 Téléchargements

Partager

Gmail Mastodon Facebook X LinkedIn More