[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

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


 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 ([EMAIL PROTECTED])
Martin Berger ([EMAIL PROTECTED])


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

Reply via email to