  Weakest precondition transformers are essential notions for program
verification, and various extensions have been studied. However, only a few
consider both higher-order languages and syntactic calculation of weakest
precondition transformers. In this paper, we consider weakest precondition
transformers for a higher-order functional language with computational effects
and recursion and show that we can calculate them via a CPS transformation. We
prove this in a general framework of categorical semantics. Because of this
generality, two existing methods for program verification can be understood as
instances of our result. Specifically, we show how to instantiate our result to
(1) verification of trace properties by Kobayashi et al. and (2) expected cost
analysis by Avanzini et al.

Logic in Computer Science