Logical Reasoning for Higher-Order Functions with Local State

Yoshida, Nobuko, Honda, Kohei and Berger, Martin (2008) Logical Reasoning for Higher-Order Functions with Local State. Logical Methods in Computer Science, 4 (4). pp. 1-68. ISSN 1860-5974

[img] PDF
Restricted to SRO admin only

Download (589kB)


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 captured logically using a predicate asserting reachability of a reference name from a possibly higher-order datum and quantifiers over hidden references. 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.

Item Type: Article
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Martin Berger
Date Deposited: 06 Feb 2012 18:43
Last Modified: 13 Mar 2017 10:54
URI: http://srodev.sussex.ac.uk/id/eprint/17926

View download statistics for this item

📧 Request an update