A logical analysis of aliasing in imperative higher-order functions

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, which 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...

• Type: Conference
• Year: 2005
• Where: ICFP
• Authors: Martin Berger, Kohei Honda, Nobuko Yoshida
• Keywords: Clean Structural Reasoning, Compositional Program Logic, Earlier Logic, ICFP 2005, Programming Languages