Higher-order abstract syntax with induction in isabelle/HOL: Formalizing the π-calculus and mechanizing the theory of contexts

Abstract

Higher-order abstract syntax is a natural way to formalize programming languages with binders, like the π -calculus, because α-conversion, instantiations and capture avoidance are delegated to the meta-level of the provers, making tedious substitutions superfluous. How- ever, such formalizations usually lack structural induction, which makes syntax-analysis impossible. Moreover, when applied in logical frame- works with object-logics, like Isabelle/HOL or standard extensions of Coq, exotic terms can be defined, for which important syntactic proper- ties become invalid. The paper presents a formalization of the π -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.