The pi-calculus, sequentiality and games

I discuss a typed pi-calculus which can embed sequential higher-order functional computation fully abstractly. Among possible topics I will concentrate on the structure of the completeness proof which uses both process algebra and game semantics. Another emphasis is on the motivation of this research: why the pi-calculus, why types, and why the sequentiality.