Cleaveland, Walter Rance II2007-04-232007-04-231987-05http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-837https://hdl.handle.net/1813/6677Sequential computation has well-understood correctness criteria and proof techniques for verifying programs, but the novelty and complexity of concurrent computation complicates a similar analysis of concurrenct programs. This thesis examines the use of a system for developing formal mathematics, the Nuprl proof development system, as a tool for reasoning about concurrency and ameliorating somewhat the complex chore of analyzing concurrent programs.16524443 bytes3090679 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report