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