Sequentiality and the π-Calculus (with K. Honda, N. Yoshida)


Abstract. 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.


Downloads: Short version. Long version (draft). BibTeX