(eng) 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 ...