Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL. Harrison, W. Master's thesis, University of California, Davis, 1992.
Mechanizing the Axiomatic Semantics for a Programming Language with Asynchronous Send and Receive in HOL [pdf]Paper  abstract   bibtex   1 download  
This thesis presents the axiomatic semantics for a simple distributed language and its mechanization in HOL. The constructs of this language include asynchronous send and synchronous receive statements as well as those basic to a sequential programming language. The language has the appearance of a system programming language that supports sequential execution extended with message-passing, and would be a suitable basis for coding distributed operating systems. Included in the mechanization are functions which generate the goals associated with the verification of simple statements in the language.

Downloads: 1