Abstract. We propose a simple compositional program logic for an imperative extension of call-by-value PCF, built on Hoare logic and our preceding work on program logics for pure higher-order functions. A central feature of the logic is its systematic use of names and operations on them. This allows precise and general description of complex higher-order imperative behaviour in assertions. The proof rules of the logic exactly follow the syntax of the language and can cleanly embed, justify and extend the standard proof rules for total correctness of Hoare logic. The logic offers a foundation for general treatment of aliasing and local state on its basis, with minimal and clean extensions. After establishing soundness, we prove that valid assertions for programs completely characterise their behaviour up to observational congruence, which is established using a variant of finite canonical forms. The use of the logic is illustrated through reasoning examples which have been hard to assert and infer using existing program logic.