================================================================================
CS-R9138   J.F. Groote & A. Ponse
           "Proof theory for muCRL"


A proof theory for the specification language muCRL (micro-CRL) is
proposed.  muCRL consists of process algebra extended with abstract
data types. The proof theory is meant to formalize the interaction
between processes and data. Furthermore it provides the means to prove
properties about these in a precise way. The proof theory has been
designed such that automatic proof checking is feasible.

A simple language is defined in which basic properties of processes and
of data can be expressed. A proof system is presented for this property
language, comprising a rule for induction, the Recursive Specification
Principle, and process algebra axioms. The proof theory is illustrated
with small examples, and a case study about a bag.

Key Words & Phrases: Proof theory for specification language, ADT
(Abstract Data Types), Process Algebra.

1985 Mathematics Subject Classification: 68Q99.
1987 CR Categories: D.2.4, D.3.1, D.3.3, F3.1.

Note: The authors are supported by the European Communities under
RACE project no. 1046, Specification and Programming Environment
for Communication Software (SPECS).
The first author is also supported by
ESPRIT Basic Research Action 3006 (CONCUR).

This document does not necessarily reflect the view of the SPECS project.