
Logic & Semantics 
I discuss a typed picalculus which can embed sequential higherorder 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 picalculus, why types, and why the sequentiality.