About Hoare Logics for Higher-Order Store | Zendy

Bernhard Reus | Zendy; Thomas Streicher | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

About Hoare Logics for Higher-Order Store

Author(s) -

Bernhard Reus,

Thomas Streicher

Publication year - 2005

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-27580-0

DOI - 10.1007/11523468_108

Subject(s) - hoare logic , soundness , computer science , programming language , separation logic , simple (philosophy) , semantics (computer science) , axiomatic semantics , operational semantics , denotational semantics , domain (mathematical analysis) , order (exchange) , code (set theory) , predicate transformer semantics , abstract interpretation , domain theory , theoretical computer science , discrete mathematics , mathematics , correctness , mathematical analysis , philosophy , epistemology , finance , set (abstract data type) , economics

We present a Hoare logic for a simple imperative while-language 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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research