TYPE-THEORETIC MODELS OF CONCURRENCY

Sequential 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 concurrent 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.

Two approaches to using Nuprl in this fashion are presented. In the first, semantic models of concurrent computation are developed in the Nuprl formalism, and the Nuprl logic is used to reason about the properties of objects in the model and to develop other logics for reasoning about objects in the semantic model. These objects represent the meanings of programs, so properties of these objects will be properties of the programs they represent. Both models are used to give a semantic account of the program constructors of Milner's CCS and Hoare's CSP, and a development of temporal logic is given in the context of one model. An actual Nuprl implementation of the other model is described.

In the second approach, a means of introducing parallelism implicitly into the Nuprl evaluation framework is presented and studied. Nuprl embodies a programming language and supplies a mechanism for conducting verified programming. Therefore, incorporating a parallel evaluation procedure for the programming language introduces a notion of verified concurrent execution into the system.