article

Open access

The receptive distributed π-calculus

Authors:

Roberto M. Amadio,

Gérard Boudol,

Cédric LhoussaineAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 25, Issue 5

Pages 549 - 577

https://doi.org/10.1145/937563.937564

Published: 01 September 2003 Publication History

Abstract

We study an asynchronous distributed π-calculus, with constructs for localities and migration. We show that a static analysis ensures the receptiveness of channel names, which, together with a simple type system, guarantees the message deliverability property. This property states that any migrating message will find an appropriate receiver at its destination locality. We argue that this distributed, receptive calculus is still expressive enough while allowing for an effective type inference à la ML.

References

[1]

Amadio, R. 1997. An asynchronous model of locality, failure, and process mobility. In Proceedings of COORDINATION'97. Lecture Notes in Computer Science, vol. 1282. Springer-Verlag, Berlin, Germany. Extended version appeared as Res. Rep. 3109. INRIA, Sophia-Antipolis, France.]]

[2]

Amadio, R., Boudol, G., and Lhoussaine, C. 1999. The receptive distributed π-calculus. In Proceedings of the FST & TCS'99 Conference. Lecture Notes in Computer Science, vol. 1738. Springer-Verlag, Berlin, Germany.]]

[3]

Amadio, R. 2000. On modeling mobility. J. Theor. Comput. Sci. 240, 1, 147--176.]]

[4]

Amadio, R., Boudol, G., and Lhoussaine, C. 2000. The distributed receptive π-calculus. Res. Rep. 4080. INRIA, Sophia-Antipolos, France.]]

[5]

Amadio, R., Boudol, G., and Lhoussaine, C. 2002. On message deliverability and non-uniform receptivity. Fundament. Informat. 53, 2, 105--129.]]

[6]

Boudol, G. 1997. Typing the use of resources in a concurrent calculus. In Proceedings of ASIAN 97. Lecture Notes in Computer Science, vol. 1345. Springer-Verlag, Berlin, Germany, 239--253.]]

[7]

Cardelli, L. and Gordon, A. 1998. Mobile ambients. In Proceedings of FoSSaCS, ETAPS 98. Lecture Notes in Computer Science, vol. 1378. Springer-Verlag, Berlin, Germany, 140--155.]]

[8]

Fournet, C. and Gonthier, G. 1996. The reflexive CHAM and the join-calculus. In Proceedings of the ACM Conference on the Principles of Programming Languages. ACM Press, New York, NY, 372--385.]]

[9]

Fournet, C., Gonthier, G., Lévy, J.-J., Maranget, L., and Rémy, D. 1996. A calculus of mobile agents. In Proceedings of CONCUR'96. Lecture Notes in Computer Science, vol. 1119. Springer-Verlag, Berlin, Germany, 406--421.]]

[10]

Hennessy, M. and Riely, J., 2002. Resource access control in systems of mobile agents. Inform. Computat. 173, 82--120.]]

[11]

Jategaonkar, J. and Mitchell, J. 1993. Type inference with extended pattern matching and subtypes. Fundament. Informat. 19, 127--166.]]

[12]

Kobayashi, N. 1998. A partially deadlock-free typed process calculus. ACM Trans. Program. Lang. Syst. 20, 2, 436--482.]]

[13]

Kobayashi, N., Pierce, B., and Turner, D. 1999. Linearity and the π-calculus. ACM Trans. Program. Lang. Syst. 21, 5, 914--947.]]

[14]

Lhoussaine, C. 2002. Réceptivité, mobilité et π-Calcul. Ph.D. dissertation. Université Aix-Marseille I, Marseilles, France.]]

[15]

Lhoussaine, C. 2003. Type inference for a distributed π-calculus. In Proceedings of ESOP'03. Lecture Notes in Computer Science, vol. 2618. Springer-Verlag, Berlin, Germany, 253--268.]]

[16]

Merro, M. and Sangiorgi, D. 1998. On asynchrony in name-passing calculi. In Proceedings of ICALP'98. Lecture Notes in Computer Science, vol. 1443. Springer-Verlag, Berlin, Germany, 856--867.]]

[17]

Remy, D. 1993. Type inference for records in a natural extension of ML. In Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design C. Gunter and J. Mitchell, Eds. Academic Press, New York, NY.]]

[18]

Sangiorgi, D. 1997. The name discipline of uniform receptiveness. In Proceedings of ICALP'97. Lecture Notes in Computer Science, vol. 1256. Springer-Verlag, Berlin, Germany, 303--313.]]

[19]

Sekiguchi, T. and Yonezawa, A. 1997. A calculus with code mobility. In Proceedings of FMOODS'97. Chapman & Hall, London, U.K.]]

[20]

Sumii, E. and Kobayashi, N. 1998. A generalized deadlock-free process calculus. In Proceedings of HLCL'98. Electron. Notes Comp. Sci. 16, 3.]]

[21]

Vasconcelos, V. 1994. Typed concurrent objects. In Proceedings of ECOOP'94. Springer Lecture Notes in Computer Science, vol. 821. Springer-Verlag, Berlin, Germany, 100--117.]]

[22]

Wand, M. 1987. Complete type inference for simple objects. In Proceedings of IEEE-LICS.]]

Cited By

Poroor JJayaraman B(2013) Modeling mobile stateful channels in Z Science of Computer Programming10.1016/j.scico.2012.10.01078:9(1470-1489)Online publication date: Sep-2013
https://doi.org/10.1016/j.scico.2012.10.010
Finderup PHüttel HKnudsen JNielsen J(2010)Linear uniform receptiveness in a pi-calculus with location failuresProceedings of the Sixteenth Symposium on Computing: the Australasian Theory - Volume 10910.5555/1862317.1862328(79-88)Online publication date: 1-Jan-2010
https://dl.acm.org/doi/10.5555/1862317.1862328
Kitamura TLin H(2007)Controlling process modularity in mobile computingProceedings of the 4th international conference on Theoretical aspects of computing10.5555/1777259.1777276(246-259)Online publication date: 26-Sep-2007
https://dl.acm.org/doi/10.5555/1777259.1777276
Show More Cited By

Index Terms

The receptive distributed π-calculus
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
      2. Syntax
    2. General programming languages
      1. Language features
        Concurrent programming structures
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Type inference for a distributed π-calculus
Special issue on 12th European symposium on programming (ESOP 2003)

We study the type inference problem for a distributed π-calculus with explicit notions of locality and migration. Location types involve names that may be bound in terms. This requires an accurate new approach. We define a notion of principal typing. We ...
Proof systems for π-calculus logics
Logic for concurrency and synchronisation

We study the problem of verifying general temporal and functional properties of mobile and dynamic process networks, cast in terms of the π-calculus. Much of the expressive power of this calculus derives from the combination of name generation and ...
The m-calculus: a higher-order distributed process calculus
POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

This paper presents a new distributed process calculus, called the M-calculus, that can be understood as a higher-order version of the Distributed Join calculus with programmable localities. The calculus retains the implementable character of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 25, Issue 5

September 2003

164 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/937563

Issue’s Table of Contents

Copyright © 2003 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 2003

Published in TOPLAS Volume 25, Issue 5

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
607
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)6

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Poroor JJayaraman B(2013) Modeling mobile stateful channels in Z Science of Computer Programming10.1016/j.scico.2012.10.01078:9(1470-1489)Online publication date: Sep-2013
https://doi.org/10.1016/j.scico.2012.10.010
Finderup PHüttel HKnudsen JNielsen J(2010)Linear uniform receptiveness in a pi-calculus with location failuresProceedings of the Sixteenth Symposium on Computing: the Australasian Theory - Volume 10910.5555/1862317.1862328(79-88)Online publication date: 1-Jan-2010
https://dl.acm.org/doi/10.5555/1862317.1862328
Kitamura TLin H(2007)Controlling process modularity in mobile computingProceedings of the 4th international conference on Theoretical aspects of computing10.5555/1777259.1777276(246-259)Online publication date: 26-Sep-2007
https://dl.acm.org/doi/10.5555/1777259.1777276
Lhoussaine C(2004)Type inference for a distributed π-calculusScience of Computer Programming10.1016/j.scico.2003.12.00350:1-3(225-251)Online publication date: 1-Mar-2004
https://dl.acm.org/doi/10.1016/j.scico.2003.12.003

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents