What’s TyCO, After All?
Maxime Gamboni · 2009
Abstract. We study the expressive power of asynchronous π-calculus with nested variants (π V a) and of TyCO by means of encodings. TyCO can be seen as a sub-calculus of π V a, in that TyCO only allows one level of variants, the only difference being that π V a requires a separate construct for analysing an input while in TyCO input and value analysis are tightly bound. Still, we can give an encoding (embedding) that is fully abstract and good. We propose a fully abstract encoding from π V a to TyCO 1