Archive for the 'Theory of contexts' Category

Reasoning on an imperative object based calculus in higher-order abstract syntax

By Alberto Ciaffaglione, Luigi Liquori and Marino Miculan, from MERLIN 2003, available from Luigi Liquori’s website:

We illustrate the benefits of using Natural Deduction in combination with weak Higher-Order Abstract Syntax for formalizing an object-based calculus with objects, cloning, method-update, types with subtyping, and side-effects, in inductive type theories such as the Calculus of Inductive Constructions. This setting suggests a clean and compact formalization of the syntax and semantics of the calculus, with an efficient management of method closures. Using our formalization and the Theory of Contexts, we can prove formally the Subject Reduction Theorem in the proof assistant Coq, with a relatively small overhead.


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.