Linearity and the pi-calculus

176Citations
Citations of this article
28Readers
Mendeley users who have this article in their library.

Abstract

The economy and flexibility of the pi-calculus make it an attractive object of theoretical study and a clean basis for concurrent language design and implementation. However, such generality has a cost: encoding higher-level features like functional computation in pi-calculus throws away potentially useful information. We show how a linear type system can be used to recover important static information about a process's behavior. In particular, we can guarantee that two processes communicating over a linear channel cannot interfere with other communicating processes. After developing standard results such as soundness of typing, we focus on equivalences, adapting the standard notion of barbed bisimulation to the linear setting and showing how reductions on linear channels induce a useful "partial confluence" of process behaviors. For an extended example of the theory, we prove the validity of a tail-call optimization for higher-order functions represented as processes.

Cite

CITATION STYLE

APA

Kobayashi, N., Pierce, B. C., & Turner, D. N. (1999). Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems, 21(5), 914–947. https://doi.org/10.1145/330249.330251

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free