Logical Reasoning for Higher-Order Functions with Local State

We introduce an extension of Hoare logic for call-by-value higher-orderfunctions with ML-like local reference generation. Local references may begenerated dynamically and exported outside their scope, may store higher-orderfunctions and may be used to construct complex mutable data structures. Thisprimitive is captured logically using a predicate asserting reachability of areference name from a possibly higher-order datum and quantifiers over hiddenreferences. We explore the logic's descriptive and reasoning power withnon-trivial programming examples combining higher-order procedures anddynamically generated local state. Axioms for reachability and local invariantplay a central role for reasoning about the examples.Comment: 68 page