Process types as a descriptive tool for interaction

We demonstrate a tight relationship between linearly typed p-calculi and typed ?-calculi by giving a type-preserving translation from the call-by-value ?µ-calculus into a typed p-calculus. The ?µ-calculus has a particularly simple representation as typed mobile processes. The target calculus is a simple variant of the linear p-calculus. We establish full abstraction up to maximally consistent observational congruences in source and target calculi using techniques from games semantics and process calculi.