Abstract
A process terminates if all its reduction sequences are finite. We propose two type systems that ensure termination of π-calculus processes.
Our first type system is purely static. It refines previous type systems by Deng and Sangiorgi by taking into account certain partial order information on names so to enhance the techniques from term rewriting (based on lexicographic and multiset orderings) that underpin the proof of termination. The second system is mixed, in that it combines a static and a dynamic analysis. During the static analysis, processes are annotated with assertions. These are then used at run time to monitor the execution of processes. An exception may be raised if certain conditions that may lead to divergence are met.
We illustrate the expressiveness of the solutions proposed with a few examples of programming idioms that were beyond reach for previous type systems.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
M. Abadi, L. Cardelli, B. C. Pierce, and G. D. Plotkin. Dynamic typing in a statically typed language. ACM Trans. Program. Lang. Syst., 13(2):237–268, 1991.
R. Demangeon, D. Hirschkoff, N. Kobayashi, and D. Sangiorgi. On the complexity of termination inference for processes. In Proceedings of TGC’07, LNCS. Springer, 2008. to appear.
Y. Deng and D. Sangiorgi. Ensuring termination by typability. Inf. Comput., 204(7):1045–1082, 2006.
F. Henglein. Dynamic typing. In Proc. of ESOP’92, volume 582 of Lecture Notes in Computer Science, pages 233–253. Springer, 1992.
T. Lindholm and F. Yellin. The JavaTM Virtual Machine Specification. Addison Wesley, 1997.
A. Marchetti-Spaccamela, U. Nanni, and H. Rohnert. Maintaining a topological order under edge insertions. Inf. Process. Lett., 59(1):53–58, 1996.
D. Sangiorgi. Termination of processes. Mathematical Structures in Computer Science, 16(1):1–39, 2006.
D. Sangiorgi and D. Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge University Press, 2001.
P. R. Wilson. Uniprocessor garbage collection techniques. In Proc. of IWMM’92, volume 637 of Lecture Notes in Computer Science, pages 1–42. Springer, 1992.
N. Yoshida, M. Berger, and K. Honda. Strong normalisation in the pi-calculus. Information and Computation, 191(2):145–202, 2004.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Demangeon, R., Hirschkoff, D., Sangiorgi, D. (2008). Static and dynamic typing for the termination of mobile processes. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, L. (eds) Fifth Ifip International Conference On Theoretical Computer Science – Tcs 2008. IFIP International Federation for Information Processing, vol 273. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-09680-3_28
Download citation
DOI: https://doi.org/10.1007/978-0-387-09680-3_28
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-387-09679-7
Online ISBN: 978-0-387-09680-3
eBook Packages: Computer ScienceComputer Science (R0)