[TYPES/announce] Logical Reasoning for Higher-Order Functions with Local State

[Nobuko Yoshida]

The following paper on Hoare Logic for imperative higher-order
functions with local state is available.

 http://www.doc.ic.ac.uk/~yoshida/paper/middle2007.pdf

 Logical Reasoning for Higher-Order Functions with Local State

by Nobuko Yoshida, Kohei Honda and Martin Berger

We shall be grateful for any comments from you.

Nobuko Yoshida (yoshida at doc.ic.ac.uk)
Kohei Honda (kohei at dcs.qmul.ac.uk)
Martin Berger (mberger at doc.ic.ac.uk)

----------------------------------------------------------
Abstract

We introduce an extension of Hoare logic for call-by-value
higher-order functions with ML-like local reference generation.  Local
references may be generated dynamically and exported outside their
scope, may store higher-order functions, and may be used to construct
complex mutable data structures. This primitive is fully captured in
the logic using a predicate which asserts reachability of a reference
name from a possibly higher-order datum and quantifiers over hidden
references.  The logic enjoys a strong match with the semantics of
programs, in the sense that valid assertions characterise the standard
contextual congruence. We explore the logic's descriptive and
reasoning power with non-trivial programming examples combining
higher-order procedures and dynamically generated local state.  Axioms
for reachability and local invariant play a central role for reasoning
about the examples.

Our previous related papers can be also found from
http://www.doc.ic.ac.uk/~yoshida/local/reference.html