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
Complete list of metadatas

https://hal-lara.archives-ouvertes.fr/hal-02101817
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:07:05 AM
Last modification on : Tuesday, May 21, 2019 - 1:28:49 AM

File

RR2000-23.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101817, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

5

Files downloads

12