About Hoare Logics for Higher-order Store

Reus, Bernhard and Streicher, Thomas (2005) About Hoare Logics for Higher-order Store. In: 32nd International Colloquium on Automata, Languages and Programming Languages (ICALP), LNCS, Lisbon.

Full text not available from this repository.
Item Type: Conference or Workshop Item (Paper)
Additional Information: 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.
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Bernhard Reus
Date Deposited: 06 Feb 2012 21:11
Last Modified: 13 Apr 2012 14:18
URI: http://sro.sussex.ac.uk/id/eprint/30039
📧 Request an update