Search

• < Previous
• 1
• Next >

Logical Reasoning for Higher-Order Functions with Local State

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.&nbsp;[&hellip;]