×

Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the \(\pi\)-calculus and mechanizing the theory of contexts. (English) Zbl 0978.68045

Honsell, Furio (ed.) et al., Foundations of software science and computation structures. 4th international conference, FOSSACS 2001, held as part of the joint European conferences on theory and practice of software, ETAPS 2001, Genova, Italy, April 2-6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2030, 364-378 (2001).
Summary: Higher-order abstract syntax is a natural way to formalize programming languages with binders, like the \(\pi\)-calculus, because \(\alpha\)-conversion, instantiations and capture avoidance are delegated to the meta-level of the provers, making tedious substitutions superfluous. However, such formalizations usually lack structural induction, which makes syntax-analysis impossible. Moreover, when applied in logical frameworks with object-logics, like Isabelle/HOL or standard extensions of Coq, exotic terms can be defined, for which important syntactic properties become invalid.
The paper presents a formalization of the \(\pi\)-calculus in Isabelle/HOL, using well-formedness predicates which both eliminate exotic terms and yield structural induction. These induction-principles are then used to derive the Theory of Contexts fully within the mechanization.
For the entire collection see [Zbl 0960.00057].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B70 Logic in computer science
PDFBibTeX XMLCite
Full Text: Link