Higher-order imperative language features have posed challenges for formal reasoning, including program verification. Due to the presence of side-effects, it is often difficult to provide adequate abstractions to support suitable summarization using standard pre/post specification.

We propose a new novel solution without the need for using abstract properties to summarise the behaviour of higher-order functions. Instead, we propose to provide logic constructs at the logic level to support imperative sequencing and effects. Together with recursion and uninterpreted relations, we are able to support arbitrarily precise specification for higher-order programs. Moreover, we are also able to support other important higher-order features, such as delimited continuations, via our extended program logics. We have implemented our prototype based on top of a heap-based separation logics; and had also freely used lemmas to support re-summarization for each instantiated higher-order function call.