On Encoding p pi in m pi

Abstract

This paper is about the encoding of p pi, the polyadic pi-calculus, in m pi, the monadic pi-calculus. A type system for m pi processes is introduced that captures the interaction regime underlying the encoding of p pi processes respecting a sorting. A full-abstraction result is shown: two p pi processes are typed barbed congruent iff their m pi encodings are monadic-typed barbed congruent.