About Hoare Logics for Higher-Order Store

Abstract. We present a Hoare logic for a simple imperative whilelanguage with stored commands, ie. stored parameterless procedures. Stores that may contain procedures are called higher-order. Soundness of our logic is established by using denotational rather than operational semantics. The former is employed to elegantly account for an inherent difficulty of higher-order store, namely that assertions necessarily describe recursive predicates on a recursive domain. In order to obtain proof rules for mutually recursive procedures, assertions have to explicitly refer to the code of the procedures.

• Type: Conference
• Year: 2005
• Where: ICALP
• Authors: Bernhard Reus, Thomas Streicher
• Keywords: Hoare Logic, ICALP 2005, Parameterless Procedures, Simple Imperative Whilelanguage, Theoretical Computer Science