Skip to main content
SpringerLink
Log in

Predicative polymorphism in π-calculus

  • Conference paper
  • First Online:
PARLE'94 Parallel Architectures and Languages Europe (PARLE 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 817))

Abstract

We present a formulation of the polyadic π-calculus featuring a syntactic category for agents, together with a typing system assigning polymorphic types to agents. The new presentation introduces an operator to express recursion, and an ML-style let-constructor allowing to associate an agent to an agent-variable, and use the latter several times in a program. The essence of the monomorphic type system is the assignment of types to names, and multiple name-type pairs to programs [14]. The polymorphic type system incorporates a form of abstraction over types, and inference rules allowing to introduce and eliminate the abstraction operator. The extended system preserves most of the syntactic properties of the monomorphic system, including subject-reduction and computability of principal typings. We present an algorithm to extract the principal typing of a process, and prove it correct with respect to the typing system. We also study, in the context of π-calculus, some well-known properties of the let-constructor.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Luis Damas and Robin Milner. Principal type-schemes for functional programs. In 9th ACM Symposium on Principles of Programming Languages, pages 207–212, 1982.

    Google Scholar 

  2. Kohei Honda. Types for dyadic interaction. In 4th International Conference on Concurrency Theory, volume 715 of LNCS, pages 509–523. Springer-Verlag, August 1993.

    Google Scholar 

  3. Paris C. Kanellakis, Harry G. Mairson, and John C. Mitchell. Unification and ML type reconstruction. In Computational Logic, Essays in Honor of Alan Robinson, pages 444–478. MIT Press, 1991.

    Google Scholar 

  4. A. J. Kfoury, J. Tiuryn, and P. Urzyczyn. A proper extension of ML with an effective type-assignment. In 15th ACM Symposium on Principles of Programming Languages, pages 58–69, 1988.

    Google Scholar 

  5. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

    Article  Google Scholar 

  6. Robin Milner. Functions as processes. In Automata, Language and Programming, volume 443 of LNCS. Springer-Verlag, 1990. Also as Rapport de Recherche No 1154, INRIA-Sophia Antipolis, February 1990.

    Google Scholar 

  7. Robin Milner. The polyadic π-calculus: a tutorial. ECS-LFCS 91-180, University of Edinburgh, October 1991.

    Google Scholar 

  8. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and II. Information and Computation, 100:1–77, 1992. Also as Tech. Rep. ECS-LFCS 89-85/86, University of Edinburgh.

    Article  Google Scholar 

  9. John C. Mitchell. Type systems for programming languages. In Handbook of Theoretical Computer Science, pages 366–358. Elsevier Science Publishers B.V., 1990.

    Google Scholar 

  10. A. Mycroft. Polymorphic type schemes for functional programming. In 9th ACM Symposium on Principles of Programming Languages, 1984.

    Google Scholar 

  11. Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. In 8th IEEE Symposium on Logic in Computer Science, June 1993.

    Google Scholar 

  12. Davide Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, University of Edinburgh, 1992.

    Google Scholar 

  13. David N. Turner. A π-calculus sorting discipline. University of Edinburgh, December 1992.

    Google Scholar 

  14. Vasco T. Vasconcelos and Kohei Honda. Principal typing-schemes in a polyadic π-calculus. In 4th International Conference on Concurrency Theory, volume 715 of LNCS, pages 524–538. Springer-Verlag, August 1993. Also as Keio University Report CS 92-002.

    Google Scholar 

  15. Vasco T. Vasconcelos and Mario Tokoro. A typing system for a calculus of objects. In 1st International Symposium on Object Technologies for Advanced Software, volume 742 of LNCS, pages 460–474. Springer-Verlag, November 1993.

    Google Scholar 

  16. Mitchell Wand. A simple algorithm and proof for type inference. Fundamenta Informaticae, X:115–122, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Keio University, 3-14-1 Hiyoshi Kohoku-ku, 223, Yokohama, Japan

    Vasco T. Vasconcelos

Authors
  1. Vasco T. Vasconcelos
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Costas Halatsis Dimitrios Maritsas George Philokyprou Sergios Theodoridis

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vasconcelos, V.T. (1994). Predicative polymorphism in π-calculus. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds) PARLE'94 Parallel Architectures and Languages Europe. PARLE 1994. Lecture Notes in Computer Science, vol 817. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58184-7_120

Download citation

  • DOI: https://doi.org/10.1007/3-540-58184-7_120

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58184-0

  • Online ISBN: 978-3-540-48477-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation