Skip to Main content Skip to Navigation

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 :
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 : Saturday, September 11, 2021 - 3:19:19 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⟩



Les métriques sont temporairement indisponibles