Publications (co-) authored by Rance Cleaveland: 1988 and before

R. Constable et al.

Implementing Mathematics with the NUPRL Proof Development System.

Prentice-Hall, Englewood Cliffs, New Jersey, 1986.

R. Cleaveland and M. Hennessy.

Priorities in process algebra.

In Third Annual Symposium on Logic in Computer Science (LICS '88), pages 193--202, Edinburgh, Scotland, July 1988. IEEE Computer Society Press.

An operational semantics for an algebraic theory of concurrency is developed that incorporates a notion of priority into the definition of the execution of actions. An equivalence based on strong observational equivalence is defined and shown to be a congruence, and a complete axiomatization is given for finite terms. Several examples highlight the novelty and usefulness of our approach.

Note: Only the journal version of this paper is available.

Type theory and concurrency.

International Journal of Parallel Programming, 17(2):153--206, 1988.

This paper describes the use of an automated reasoning tool, the Nuprl system, to formalize Milner's Calculus of Communicating Systems (CCS). The goals of this work are two-fold: the first is to investigate the feasibility of using systems like Nuprl to handle the formal detail arising from reasoning about concurrency, while the second is to develop a framework in which various formalisms for reasoning about concurrency may be presented in an automated fashion. To these ends, an implementation in Nuprl of a formal theory of concurrency is described, an implementation of CCS in this mechanized semantic theory presented, and two means of analyzing CCS terms are investigated.

Last modified: August 13, 1998