Nobuko Yoshida ; Kohei Honda ; Martin Berger - Logical Reasoning for Higher-Order Functions with Local State

lmcs:830 - Logical Methods in Computer Science, October 20, 2008, Volume 4, Issue 4 - https://doi.org/10.2168/LMCS-4(4:2)2008
Logical Reasoning for Higher-Order Functions with Local State

Authors: Nobuko Yoshida ; Kohei Honda ; Martin Berger

    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.


    Volume: Volume 4, Issue 4
    Published on: October 20, 2008
    Accepted on: June 25, 2015
    Submitted on: September 23, 2007
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,D.3.3,D.3.2,F.3.1,F.3.2,F.4.1

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1017/s095679681200024x
    Source : ScholeXplorer IsReferencedBy DOI 10.1145/1863543.1863566
    Source : ScholeXplorer IsReferencedBy DOI 10.1145/1932681.1863566
    • 10.1017/s095679681200024x
    • 10.1017/s095679681200024x
    • 10.1145/1932681.1863566
    • 10.1145/1863543.1863566
    • 10.1145/1863543.1863566
    The impact of higher-order state and control effects on local relational reasoning
    NeisGeorg ; DreyerDerek ; BirkedalLars ;

    5 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 424 times.
    This article's PDF has been downloaded 683 times.