Logical Reasoning for Higher-Order Functions with Local State

DOI10.1007/978-3-540-71389-0_26MaRDI QIDQ5758044zbMATH OpenOpenAlexFDO

Authors Nobuko Yoshida, Kohei Honda, Martin Berger

Publication date 7 September 2007

Published in Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71389-0_26

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Logical Reasoning for Higher-Order Functions with Local State
• Automata, Languages and Programming
• Operational reasoning for functions with local state
• Program logics for sequential higher-order control
• Hoare logic for higher order store using simple semantics

Cited in

(11)

• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• Program logics for sequential higher-order control
• An observationally complete program logic for imperative higher-order functions
• Weak updates and separation logic
• The impact of higher-order state and control effects on local relational reasoning
• Operational reasoning for functions with local state
• A functional logic for higher level reasoning about computation
• Descriptive and Relative Completeness of Logics for Higher-Order Functions
• Logical Reasoning for Higher-Order Functions with Local State
• The impact of higher-order state and control effects on local relational reasoning
• Local local reasoning: a BI-hyperdoctrine for full ground store

This page was built for publication: Logical Reasoning for Higher-Order Functions with Local State

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5758044)