Proofs by annotations for a simple data-parallel language

Abstract : We present a proof outline generation system for a simple data-parallel kernel language called L. We show that proof outlines are equivalent to the sound and complete Hoare logic defined for L in previous papers. Proof outlines for L are very similar to those for usual scalar-like languages. In particular, they can be mechanically generated backwards from the final post-assertion of the program. They appear thus as a valuable basis to implement a validation assistance tool for data-parallel programming.
Document type :
Reports
Complete list of metadatas

Cited literature [9 references]  Display  Hide  Download

https://hal-lara.archives-ouvertes.fr/hal-02102026
Contributor : Colette Orange <>
Submitted on : Wednesday, April 17, 2019 - 9:12:20 AM
Last modification on : Sunday, April 28, 2019 - 1:23:05 AM

File

RR1995-08.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02102026, version 1

Collections

Citation

Luc Bougé, David Cachera. Proofs by annotations for a simple data-parallel language. [Research Report] LIP RR-1995-08, Laboratoire de l'informatique du parallélisme. 1995, 2+19p. ⟨hal-02102026⟩

Share

Metrics

Record views

12

Files downloads

13