Deriving Proof Rules from Continuation Semantics
1999
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.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
10
References
6
Citations
NaN
KQI