Deriving Proof Rules Form Continuations Semantics
Philippe Audebaud, Elena Zucca · HAL (Le Centre pour la Communication Scientifique Directe) · 1997
We claim that the continuation style semantics of a programming language can provide a starting point for constructing a proof system for that language. The basic idea is to see weakest precondition as a particular instance of continuation style semantics, hence to interpret correctness assertions (e.g. Hoare triples {p}C{r}) as inequalities over continuations. This approach also shows a correspondence between labels in a program and annotations.