A framework for parallel program refinement
In TACAS, pages
This paper presents a formal framework for developing provably
correct parallel programs through refinements. We formalize rigorously, with
respect to typing, some imperative programming constructs and propose
refinements of them. Moreover, we try to make the semantics denotation as
close as possible to the usual programming notation; the aim being to make
easy the reasoning at the semantics level. This formalization is embedded
within the HOL interactive theorem prover and consequently reusable as a
framework for general programming by refinement.
IRIT, Toulouse, France.
Available as PostScript.
BRICS WWW home page