Deriving Proof Rules from Continuation Semantics
Philippe Audebaud, Elena Zucca · Formal Aspects of Computing · 1999
Abstract. We claim that a continuation style semantics of a programming language can provide a starting point for constructing its proof system. The basic idea is to see weakest preconditions 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.