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 part of data structures. The logic extends our previous work with new modal operators which serve as building blocks for clean structural reasoning about higher-order programs and data structures in the presence of aliasing. 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.