Typing the use of resources in a concurrent calculus

Extended abstract
  • Gérard Boudol
Session 6
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


We introduce a new type system for the blue calculus - a variant of the π-calculus that directly contains the Λ-calculus. Our notion of type is built upon a combination of Curry-Church simple types and Hennessy-Milner logic with recursion. We interpret a modality (u)T as the type of a process offering a resource of type T on the name u. In the typing system this is used in a kind of logical cut rule, ensuring that a message to the name u will meet a corresponding offer. We show that our calculus is type safe, that is, types are preserved along the computations.


Parallel Composition Side Condition Linear Zone Schedule Variable Subject Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    S. Abramsky, S. Gay, R. Nagarajan, Interaction categories and the foundations of typed concurrent programming, in Deductive Program Design (M. Broy, Ed), NATO ASI Series F (1995).Google Scholar
  2. [2]
    R. Amadio, An asynchronous model of locality, failure, and process mobility, INRIA Res. Report 3109 (1997) to appear in the Proceedings of the Conference COORDINATION'97.Google Scholar
  3. [3]
    R. Amadio, M. Dam, Toward a modal theory of types for the π-calculus, Formal Techniques in Real-Time and Fault Tolerant Systems'96, Lecture Notes in Comput. Sci. 1135 (1996).Google Scholar
  4. [4]
    G. Berry, G. Boudol, The chemical abstract machine, Theoretical Comput. Sci. 96 (1992) 217–248.CrossRefGoogle Scholar
  5. [5]
    G. Boudol, The π-calculus in direct style, POPL'97 (1997) 228–241.Google Scholar
  6. [6]
    F. Cardone, M. Coppo, Two extensions of Curry's type inference system, in Logic and Computer Science (P. Odifreddi, Ed.), Academic Press (1990) 19–75.Google Scholar
  7. [7]
    C. Fournet, G. Gonthier, The reflexiveCham, and the join calculus, POPL'96 (1996) 372–385.Google Scholar
  8. [8]
    J.-Y. Girard, Linear Logic, Theoretical Comput. Sci. 50 (1987) 1–102.CrossRefGoogle Scholar
  9. [9]
    J.-Y. Girard, On the unity of logic, Annals of Pure and Applied Logic 59 (1993) 201–217.CrossRefGoogle Scholar
  10. [10]
    M. Hennessy, R. Milner, Algebraic laws for nondeterminism and concurrency, JACM 32 (1985) 137–161.CrossRefGoogle Scholar
  11. [11]
    N. Kobayashi, B. Pierce, D. Turner, Linearity and the π-calculus, POPL'96 (1996) 358–371.Google Scholar
  12. [12]
    N. Kobayashi, A partially deadlock-free typed process calculus, Proceedings of LICS'97 (1997) 128–139.Google Scholar
  13. [13]
    K. G. Larsen, Proof systems for satisfiability in Hennessy-Milner logic with recursion, Theoretical Comput. Sci. 72 (1190) 265–288.CrossRefGoogle Scholar
  14. [14]
    M. Miculan, F. Gadduci, Modal μ,-types for processes, LICS'95 (1995) 221–231.Google Scholar
  15. [15]
    R. Milner, J. Parrow, D. Walker, A calculus of mobile processes, Information and Computation 100 (1992) 1–77.CrossRefGoogle Scholar
  16. [16]
    R. Milner, The polyadic π-calculus: a tutorial, Technical Report ECSLFCS-91-180, Edinburgh University (1991) Reprinted in Logic and Algebra of Specification, F. Bauer, W. Brauer and H. Schwichtenberg, Eds, Springer Verlag, 1993, 203–246.Google Scholar
  17. [17]
    O. Nierstrasz, Composing Active Objects, In Research Directions in Concurrent Object-Oriented Programming (G. Agha, P. Wegner and A. Yonezawa Eds), MIT Press (1993) 151–171.Google Scholar
  18. [18]
    O. Nierstrasz, Regular Types for Active Objects, Chapter 4 of Object-Oriented Software Composition (O. Nierstrasz and D. Tsichritzis, Eds), Prentice Hall (1995) 99–121.Google Scholar
  19. [19]
    B. Pierce, Programming in the π-calculus — A Tutorial Introduction to Pict, available electronically, Computer Science Department, Indiana University (1997)Google Scholar
  20. [20]
    K. Takeuchi, K. Honda, M. Kubo, An interaction-based language and its typing system, PARLE'94, Lecture Notes in Comput. Sci. 817 (1994).Google Scholar
  21. [21]
    D. Turner, The Polymorphic Pi-calculus: Theory and Implementation, Ph.D. Thesis, University of Edinburgh (1995).Google Scholar
  22. [22]
    N. Yoshida, Graph types for monadic mobile processes, FST-TCS'96, Lecture Notes in Comput. Sci. 1180 (1996) 371–386.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Gérard Boudol
    • 1
  1. 1.INRIA Sophia-AntipolisSophia Antipolis CedexFrance

Personalised recommendations