Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Reports

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 metadata

Cited literature [21 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02101852
Contributor : Colette ORANGE Connect in order to contact the contributor
Submitted on : Wednesday, April 17, 2019 - 9:08:05 AM
Last modification on : Saturday, September 11, 2021 - 3:19:19 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

4

Files downloads

6