One way of enforcing an information flow control policy is to use a static type system capable of guaranteeing a noninterference property. Noninterference requires that two processes with distinct "high"-level components, but common "low"-level structure, cannot be distinguished by "low"-level observers. We state this property in terms of a rather strict notion of process equivalence, namely weak barbed reduction congruence.

Because noninterference is not a safety property, it is often regarded as more difficult to establish than a conventional type safety result. This paper aims to provide an elementary noninterference roof in the setting of the π calculus. This is done by reducing the problem to subject reduction "a safety property" for a nonstandard, but fairly natural, extension of the π calculus, baptized the (π)-calculus.