Deriving Proof Rules Form Continuations Semantics

Abstract : 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.
Document type :
Reports
Complete list of metadatas

Cited literature [21 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101852
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:08:05 AM
Last modification on : Wednesday, November 20, 2019 - 2:51:57 AM

File

RR1997-19.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02101852, version 1

Collections

Citation

Philippe Audebaud, Elena Zucca. Deriving Proof Rules Form Continuations Semantics. [Research Report] LIP RR-1997-19, Laboratoire de l'informatique du parallélisme. 1997, 2+19p. ⟨hal-02101852⟩

Share

Metrics

Record views

5

Files downloads

8