Logical Reasoning for Higher-Order Functions with Local State

TL;DR

This paper extends Hoare logic to handle higher-order functions with local state, enabling formal reasoning about complex mutable data structures in functional programming languages.

Contribution

It introduces a novel logical framework that captures dynamic local reference generation and higher-order state manipulation, enhancing reasoning capabilities.

Findings

Logic can express reachability of references

Enables reasoning about complex mutable data structures

Demonstrates reasoning with non-trivial programming examples

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 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.