Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the pi-calculus and mechanizing the Theory of Contexts

By Christine Roeckl, Daniel Hirchskoff and Stefan Berghofer, from FOSSACS 2001, available from Christine Roeckl’s website:

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.

Proof scripts are available here.

0 Responses to “Higher-order abstract syntax with induction in Isabelle/HOL: formalizing the pi-calculus and mechanizing the Theory of Contexts”



  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: