Levin, Gary Marc2007-04-232007-04-231979-11http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR79-401https://hdl.handle.net/1813/7514We present proof rules for an extension of the Communicating Sequential Processes proposed by Hoare. The send and receive statements are treated symmetrically, simplifying the rules and allowing send to appear in guards. An example is given to explain the use of the technique. This is an outline of a substantial part of a PhD thesis that is expected to be completed in June 1980.1322530 bytes411902 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report