Mobile Processes and Termination

  • Romain Demangeon
  • Daniel Hirschkoff
  • Davide Sangiorgi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5700)


This paper surveys some recent works on the study of termination in a concurrent setting. Processes are π-calculus processes, on which type systems are imposed that ensure termination of the process computations. Two approaches are exposed. The first one draws on the method of logical relations, which has been extensively used in the analysis of sequential languages. The second approach exploits notions from term rewriting.


Normal Form Type System Logical Relation Logical Predicate Parallel Composition 
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. [BL00]
    Boudol, G., Laneve, C.: λ-calculus, multiplicities and the π-calculus. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge (2000)Google Scholar
  2. [Bou08]
    Boutillier, P.: Implementation of a hybrid type system for termination in the π-calculus. Training period report, ENS Lyon (2008)Google Scholar
  3. [DCdLP94]
    Dezani-Ciancaglini, M., de Liguoro, U., Piperno, U.: Fully abstract semantics for concurrent λ-calculus. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 16–35. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  4. [DH95]
    Dershowitz, N., Hoot, C.: Natural termination. Theoretical Computer Science 142(2), 179–207 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  5. [DHKS07]
    Demangeon, R., Hirschkoff, D., Kobayashi, N., Sangiorgi, D.: On the Complexity of Termination Inference for Processes. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol. 4912, pp. 140–155. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. [DHS08]
    Demangeon, R., Hirschkoff, D., Sangiorgi, D.: Static and Dynamic Typing for the Termination of Mobile Processes. In: Proc. of IFIP TCS 2008. IFIP, vol. 273, pp. 413–427. Springer, Heidelberg (2008)Google Scholar
  7. [DM79]
    Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)MathSciNetCrossRefzbMATHGoogle Scholar
  8. [DS06a]
    Deng, Y., Sangiorgi, D.: Ensuring Termination by Typability. Information and Computation 204(7), 1045–1082 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  9. [DS06b]
    Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Inf. Comput. 204(7), 1045–1082 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  10. [FG96]
    Fournet, C., Gonthier, G.: The Reflexive Chemical Abstract Machine and the Join calculus. In: Proc. 23th POPL. ACM Press, New York (1996)Google Scholar
  11. [Gan80]
    Gandy, R.O.: Proofs of strong normalization. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, London (1980)Google Scholar
  12. [Kob98]
    Kobayashi, N.: A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems 20(2), 436–482 (1998)CrossRefGoogle Scholar
  13. [Kob07]
    Kobayashi, N.: TyPiCal: Type-based static analyzer for the Pi-Calculus (2007),
  14. [Mer01]
    Merro, M.: Locality in the π-calculus and applications to object-oriented languages. PhD thesis, Ecoles des Mines de Paris (2001)Google Scholar
  15. [Mil99]
    Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar
  16. [Mit96]
    Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)Google Scholar
  17. [Mos01]
    Mosses, P.D.: The varieties of programming language semantics. In: Bjørner, D., Broy, M., Zamulin, A.V. (eds.) PSI 2001. LNCS, vol. 2244, pp. 165–190. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  18. [Mos04]
    Mosses, P.D.: Exploiting labels in structural operational semantics. Fundam. Inform. 60(1-4), 17–31 (2004)MathSciNetzbMATHGoogle Scholar
  19. [Mos06]
    Mosses, P.D.: Formal semantics of programming languages: - an overview -. Electr. Notes Theor. Comput. Sci. 148(1), 41–73 (2006)CrossRefGoogle Scholar
  20. [RDS09]
    Demangeon, R., Hirschkoff, D., Sangiorgi, D.: Termination in Higher-Order Concurrent Calculi. In: Proc. of FSEN 2009 (to appear, 2009)Google Scholar
  21. [San99]
    Sangiorgi, D.: The name discipline of uniform receptiveness. Theo. Comp. Sci. 221, 457–493 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  22. [San06]
    Sangiorgi, D.: Termination of processes. Mathematical Structures in Computer Science 16(1), 1–39 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  23. [SW01a]
    Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  24. [SW01b]
    Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  25. [Tur96]
    Turner, N.D.: The polymorphic pi-calculus: Theory and Implementation. PhD thesis, Department of Computer Science, University of Edinburgh (1996)Google Scholar
  26. [YBK01]
    Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the π-Calculus. In: 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pp. 311–322. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Romain Demangeon
    • 1
  • Daniel Hirschkoff
    • 1
  • Davide Sangiorgi
    • 2
  1. 1.ENS LyonUniversité de Lyon, CNRS, INRIAFrance
  2. 2.INRIA and Università di BolognaItaly

Personalised recommendations