We present a 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 are together used
to establish full abstraction.
Posted to theory by Ehud Lamm on 8/14/01; 12:34:02 AM
|
|