University of Sussex
Browse

File(s) not publicly available

About Hoare logics for higher-order store

presentation
posted on 2023-06-08, 09:09 authored by Bernhard ReusBernhard Reus, Thomas Streicher
No description supplied

History

Publication status

  • Published

ISSN

0302-9743

Publisher

Springer

Volume

3580

Pages

12.0

Presentation Type

  • paper

Event name

32nd International Colloquium on Automata, Languages and Programming Languages (ICALP), LNCS

Event location

Lisbon

Event type

conference

ISBN

3-540-27580-0

Department affiliated with

  • Informatics Publications

Notes

Originality: discusses a new program logic for a language with general updatable code pointers; can deal with recursion through the store. Rigour: denotational model and soundness proof using results about existence of recursive predicates, Significance/Impact: provides the first deduction rule for "recursion through the store". It allows one to do formal reasoning on languages that use code pointers. This is e.g. used in device drivers written in C. Hongseok Yang (EPSRC advanced research fellow) investigates this and a joint co-operation with him has been started. It has spawned further research on new logics for object-oriented languages that implicitly use code pointers (project proposal in preparation). Impact: it may lead to program logics for languages with code pointers like C or even languages with advanced features that can be modeled by code pointers (for example aspect-oriented languages or dynamic class loading). Birkedal (Copenhagen) and Yang (Queen Mary) have been interested and are now collaborating with us. Outlet/citations: ICALP is a top long running (over 32 years) international conference and Track B had < 32% acceptance rate that year.

Full text available

  • No

Peer reviewed?

  • Yes

Editors

L Monteior, L Caires, C Palamidessi, GF Italiano, M Yung

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC