University of Sussex
Browse
ICALP05.pdf (171.56 kB)

About Hoare logics for higher-order store

Download (171.56 kB)
chapter
posted on 2023-06-07, 14:13 authored by Bernhard ReusBernhard Reus, Thomas Streicher
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. Both authors have been partially supported by APPSEM II (Applied Semantics), a thematic network funded by the IST programme of the European Union, IST-2001-38957.

History

Publication status

  • Published

Publisher

Springer Verlag

Volume

3580

Page range

1337-1348

Pages

1477.0

Book title

Automata, Languages and Programming: Proceedings of the 32nd International Colloquim, ICALP 2005, Lisbon, Portugal

Place of publication

Berlin, Germany

ISBN

9783540275800

Series

Lecture Notes in Computer Science

Department affiliated with

  • Informatics Publications

Notes

Publisher's version available at official url

Full text available

  • Yes

Peer reviewed?

  • Yes

Editors

M. Yung, L. Caires, C. Palamidessi, L. Monteiro, G.F. Italiano

Legacy Posted Date

2007-08-13

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC