Computing Publications

Publications Home » A Logical Analysis of Aliasing in...

A Logical Analysis of Aliasing in Imperative Higher-Order Functions

Martin Berger, Kohei Honda, Nobuko Yoshida

Conference or Workshop Paper
ICFP'05, Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming
September, 2005
pp.280–293
ACM Press
Abstract

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.

BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.