Logical Reasoning for Higher-Order Functions with Local State (with Nobuko Yoshida and Kohei Honda)

We introduce an extension of Hoare logic for imperative higher-order functions with local state and full aliasing. Local state may be generated dynamically and exported outside its scope, may store higher-order functions, and may be used to construct complex shared mutable data structures. The logic is built on the authors' previous study on Hoare logics for imperative higher-order functions and aliasing. Complex behaviour induced by local state is captured with a minimal syntax extension: a first order predicate which asserts reachability of reference names. After establishing soundness and observational completeness, we explore the logic's descriptive and reasoning power with non-trivial examples, offering effective reasoning principles for a general class of higher-order behaviours in the presence of local state.

Extended abstract: pdf. Status: published (bibtex).
Full version: pdf. Status: published.
Proof of completeness results: pdf Status: unpublished.

More information about this line of work can be found here.

$Id: index.html,v 1.7 2007/09/11 13:36:13 mberger Exp mfb21 $