Sciweavers

Share
FOSSACS
2007
Springer

Logical Reasoning for Higher-Order Functions with Local State

11 years 11 months ago
Logical Reasoning for Higher-Order Functions with Local State
Abstract. We introduce an extension of Hoare logic for call-by-value higherorder functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their scope, may store higherorder functions and may be used to construct complex mutable data structures. This primitive is captured logically using a predicate asserting reachability of a reference name from a possibly higher-order datum and quantifiers over hidden references. The logic enjoys three completeness properties: relative completeness, a logical characterisation of the contextual congruence and derivability of characteristic formulae. 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.
Nobuko Yoshida, Kohei Honda, Martin Berger
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FOSSACS
Authors Nobuko Yoshida, Kohei Honda, Martin Berger
Comments (0)
books