Higher-Order Weakest Precondition Transformers via a CPS Transformation

TL;DR

This paper establishes a syntactic relationship between weakest precondition transformers and CPS transformations for higher-order functional languages, enabling effectful program verification to be reduced to pure program verification.

Contribution

It introduces a novel syntactic framework linking weakest precondition transformers with CPS transformations, facilitating verification of effectful higher-order programs.

Findings

Reduces effectful program verification to pure program verification

Captures existing verification methods as instances of the framework

Extends weakest precondition transformers to higher-order probabilistic programs

Abstract

Weakest preconditions are a useful notion for program verification as they reduce a problem of program verification to a problem of constraint solving. Category-theoretic generalisations of weakest preconditions have been studied to capture various computational effects and various properties in a unified framework. In this paper, we propose a novel and general relationship between weakest precondition transformers and CPS transformations for higher-order functional languages with general computational effects and recursion. Technically, this gives a syntactic counterpart of the categorically-defined generic weakest precondition transformer in [Aguirre & Katsumata, 2020]. The usefulness of our results is threefold. (1) Since CPS transformations purify effectful programs, various verification problems for effectful programs can be reduced to verification problems for pure programs. This syntactic reduction makes it easier to solve the verification problems and potentially facilitates combinations with other sophisticated verification methods tailored for pure programs. (2) We capture two existing verification methods, namely, verification of event sequences [Kobayashi et al., 2018] and expected cost [Avanzini et al., 2021] as instances of our framework. (3) Our results streamline the process of extending weakest precondition transformers for imperative programs to those for higher-order programs. We show two such extensions: analysis of higher moments of cost and the conditional weakest pre-expectation for higher-order probabilistic programs. These extensions demonstrate that our theoretical framework can produce novel verification methods.