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 TeX, intuitively the minimal symmetrical conservative extension of π with input/output types. We prove some duality properties for TeX and we study embeddings between TeX and π in both directions. As an example of application of the dualities, we exploit the dualities of TeX 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
Duality and i/o-Types in the π-Calculus / Daniel Hirschkoff;Jean-Marie Madiot;Davide Sangiorgi. - STAMPA. - 7454:(2012), pp. 302-316. (Intervento presentato al convegno 23rd International Conference, CONCUR 2012 tenutosi a Newcastle upon Tyne, UK nel September 4-7, 2012) [10.1007/978-3-642-32940-1_22].
Duality and i/o-Types in the π-Calculus
SANGIORGI, DAVIDE
2012
Abstract
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 TeX, intuitively the minimal symmetrical conservative extension of π with input/output types. We prove some duality properties for TeX and we study embeddings between TeX and π in both directions. As an example of application of the dualities, we exploit the dualities of TeX 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 otherI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
