LFCS Seminar: Tuesday, 2 May - Satoshi Kura


Title:          Higher-Order Weakest Precondition Transformers via a CPS Transformation




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.

May 02 2023 -

LFCS Seminar: Tuesday, 2 May - Satoshi Kura

Satoshi Kura, National Institute of Informatics, Japan and visiting researcher at the University of Oxford https://group-mmm.org/~skura/

Venue: IF G.03