Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Towards a Formalization of pi-calculus Processes in Higher Order Abstract Syntax

Abstract : 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.
Document type :
Reports (Research report)
Complete list of metadata
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:07:05 AM
Last modification on : Wednesday, October 26, 2022 - 8:14:47 AM


Files produced by the author(s)


  • HAL Id : hal-02101817, version 1



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⟩



Record views


Files downloads