From higher-order π-calculus to π-calculus in the presence of static operators

Some applications of higher-order processes require better control of communication capabilities than what is provided by the pi-calculus primitives. In particular we have found the dynamic restriction operator of CHOCS, here called blocking, useful. We investigate the consequences of adding static operators such as blocking to the first and higher-order pi-calculus. In the presence of the blocking operator (and static operators in general) the higher-order reduction of Sangiorgi, used to demonstrate the reducibility of higher-order communication features to first-order ones, breaks down. We show, as our main result, that the higher-order reduction can be regained, using an approach by which higher-order communications are replaced, roughly, by the transmission and dynamic interpretation of syntax trees. However, the reduction is very indirect, and not usable in practice. This throws new light on the position that higher-order features in the pi-calculus are superfluous and not needed in practice.