Proof theory for $ mu $ -CRL
Jan Friso Groote, Alban Ponse · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1991
A proof theory for the specification language µCRL (micro CRL) is proposed.µCRL consists of process algebra extended with abstract data types.The proof theory is meant to formalize the interaction between processes and data.Furthermore it provideo 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 sy~m 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.