Personal tools
You are here: Home Events Abstract Archives 2005 A Logical Analysis of Aliasing in Imperative Higher-Order Functions

A Logical Analysis of Aliasing in Imperative Higher-Order Functions

Martin Berger Queen Mary, University of London 4pm Tuesday 6th December 2005 Room 2511, JCMB, King's Buildings

(Joint work with Nobuko Yoshida and Kohei Honda)

We present a compositional program logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data structures. The program logic extends our earlier logic for alias-free imperative higher-order functions with new modal operators which serve as building blocks for clean structural reasoning about programs and data structures in the presence of aliasing. This has been an open issue since the pioneering work by Cartwright-Oppen and Morris twenty-five years ago. We illustrate usage of the logic for description and reasoning through concrete examples including a higher-order polymorphic Quicksort. The logical status of the new operators is clarified by translating them into (in)equalities of reference names. The logic is observationally complete in the sense that two programs are observationally indistinguishable iff they satisfy the same set of assertions.

Document Actions