Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-25T19:35:34.478Z Has data issue: false hasContentIssue false
  • English
  • Français

Termination in a π-calculus with subtyping

Published online by Cambridge University Press:  09 January 2015

IOANA CRISTESCU  and
DANIEL HIRSCHKOFF
IOANA CRISTESCU
Affiliation:
Laboratoire PPS, Université Paris Diderot and CNRS, UMR 7126, F-75205 Paris, France
DANIEL HIRSCHKOFF
Affiliation:
École Normale Supérieure de Lyon, CNRS, INRIA, UCBL, U. Lyon, France Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We present a type system to guarantee termination of π-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels.

Our type system is based on Deng and Sangiorgi's level-based analysis of processes. We show that the addition of i/o-types makes it possible to typecheck processes where a form of level polymorphism is at work. We discuss to what extent this programming idiom can be treated by previously existing proposals. We demonstrate how our system can be extended to handle the encoding of the simply-typed λ-calculus, and discuss questions related to type inference.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 8: Special Issue: Express'11 , December 2016 , pp. 1395 - 1432
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abadi, M. (1999) Protection in programming-language translations. In: Secure Internet Programming, Security Issues for Mobile and Distributed Objects. Springer Lecture Notes in Computer Science 1603 19–34.Google Scholar
Cristescu, I. and Hirschkoff, D. (2011) Termination in a pi-calculus with subtyping. In: Luttik, B. and Valencia, F. (eds.) Proceedings of EXPRESS'11. Electronic Proceedings in Theoretical Computer Science 64 44–58.Google Scholar
Demangeon, R. (2010) Terminaison des systèmes concurrents, Ph.D. thesis, ENS Lyon, 2010.Google Scholar
Demangeon, R., Hirschkoff, D., Kobayashi, N. and Sangiorgi, D. (2007) On the complexity of termination inference for processes. In: Proceedings of TGC'07. Springer Lecture Notes in Computer Science 4912 140–155.Google Scholar
Demangeon, R., Hirschkoff, D. and Sangiorgi, D. (2009) Mobile processes and termination. In: Semantics and Algebraic Specification. Springer Lecture Notes in Computer Science 5700 250–273.Google Scholar
Demangeon, R., Hirschkoff, D. and Sangiorgi, D. (2010) Termination in impure concurrent languages. In: Proceedings of CONCUR'10. Springer Lecture Notes in Computer Science 6269 328–342.CrossRefGoogle Scholar
Deng, Y. and Sangiorgi, D. (2006) Ensuring termination by typability. Information and Computation 204 (7) 1045–1082.CrossRefGoogle Scholar
Ericsson Computer Science Laboratory. (2012) Erlang programming language website. Available at http://www.erlang.org.Google Scholar
Hennessy, M. and Rathke, J. (2004) Typed behavioural equivalences for processes in the presence of subtyping. Mathematical Structures in Computer Science 14 (5) 651–684.CrossRefGoogle Scholar
Igarashi, A. and Kobayashi, N. (2000) Type reconstruction for linear π-calculus with i/o subtyping. Information and Computation 161 (1) 1–44.Google Scholar
Kobayashi, N. and Sangiorgi, D. (2010) A hybrid type system for lock-freedom of mobile processes. ACM Transactions on Programming Languages and Systems 32 (5) 1–49.Google Scholar
Mandel, L. and Maranget, L. (2012) The JoCaml programming language. Available at http://jocaml.inria.fr.Google Scholar
Pierce, B. C. and Sangiorgi, D. (1996) Typing and subtyping for mobile processes. Mathematical Structures in Computer Science 6 (5) 409–453.Google Scholar
Sangiorgi, D. (2006) Termination of processes. Mathematical Structures in Computer Science 16 (1) 1–39.Google Scholar
Sangiorgi, D. and Walker, D. (2001) The π-Calculus: A Theory of Mobile Processes, Cambridge: Cambridge University Press.Google Scholar
Vasconcelos, V. T. and Honda, K. (1993) Principal typing schemes in a polyadic pi-calculus. In: Proceedings of CONCUR'93. Springer Lecture Notes in Computer Science 715 524–538.Google Scholar
Yoshida, N., Berger, M. and Honda, K. (2004) Strong normalisation in the Pi-calculus. Information and Computation 191 (2) 145–202.Google Scholar