Martin Berger, Kohei Honda, Nobuko Yoshida
 

We present a simple type discipline for the pi-calculus which precisely captures
the notion of sequential functional computation as a specific class of name passing
interactive behaviour. The typed calculus allows direct interpretation of both
call-by-name and call-by-value sequential functions. The precision of the
representation is demonstrated by way of a fully abstract encoding of PCF. The
result shows how a typed pi-calculus can be used as a descriptive tool for a
significant class of programming languages without losing the latter's semantic
properties. Close correspondence with games semantics and process-theoretic
reasoning techniques is together used to establish full abstraction.