Theories that are designed to reason about processes and the information they exchange usually also include a construction to quantify over this information. We mention the input prefix mechanism of, e.g., the $pi$-calculus and the operation $gsum{$ for alternative quantification over data of mcrl. These constructions are implemented as binders, and hence imply a relatively complicated notion of substitution that takes the binding of these operations into account. As a consequence, the defining axioms of such constructions are not suitable for purely equational reasoning, or, to put it differently, proof systems for process theories that contain binders are not algebraic. In this paper, we shall define the variety of cylindric process algebras with conditionals, and we prove that, for data with built-in equality and built-in Skolem functions, it is an algebraic semantics of a subsystem of mcrl{. Thus we obtain a proof system for a class of process algebras with data and alternative quantification from which the complicated notion of substitution is eliminated.

Models of Computation (acm F.1.1), Studies of Program Constructs (acm F.3.3), Mathematical Logic (acm F.4.1)
Cylindric and polyadic algebras; relation algebras (msc 03G15), Applications of universal algebra in computer science (msc 08A70), Algebraic theory of languages and automata (msc 68Q70)
CWI
Software Engineering [SEN]

Luttik, S.P. (1999). Cylindric process algebras with conditionals give substitutionless $ p $ CRL. Software Engineering [SEN]. CWI.