Butler Lampson
Citation: Constructive Methods in Computer Science, ed.
Links: Abstract, Acrobat. Here is an HTML version created by OCR for the benefit of search engines; it is not meant for human consumption.
Email: blampson@microsoft.com. This paper is at http://research.microsoft.com.
Abstract:
These notes describe a method for specifying concurrent and distributed systems, and illustrate it with a number of examples, mostly of storage systems. The specification method is due to Lamport, and the notation is an extension, due to Nelson, of Dijkstra’s guarded commands.