Duality and i/o-Types in the pi-calculus

We study duality between input and output in the π-calculus. In dualisable versions of π, including πI and fusions, duality breaks with the addition of ordinary input/output types. We introduce π⎯⎯ , intuitively the minimal symmetrical conservative extension of π with input/output types. We prove some duality properties for π⎯⎯ and we study embeddings between π⎯⎯ and π in both directions. As an example of application of the dualities, we exploit the dualities of π⎯⎯ and its theory to relate two encodings of call-by-name λ-calculus, by Milner and by van Bakel and Vigliotti, syntactically quite different from each other.