Abstract
An impure language is one that combines functional and imperative constructs. We propose a method for ensuring termination of impure concurrent languages that makes it possible to combine term rewriting measure-based techniques with traditional approaches for termination in functional languages such as logical relations. The method can be made parametric on the termination technique employed on the functional part; it can also be iterated.
We illustrate the method in the case of a π-calculus with both functional and imperative names, and show that, with respect to previous approaches to termination, it allows us to extend considerably the set of processes that can be handled.
The method can also be applied to sequential languages, e.g., λ-calculi with references.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amadio, R.: On Stratified Regions. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 210–225. Springer, Heidelberg (2009)
Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 24–39. Springer, Heidelberg (2004)
Boudol, G.: Fair Cooperative Multithreading. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 272–286. Springer, Heidelberg (2007)
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)
Demangeon, R., Hirschkoff, D., Sangiorgi, D.: Appendix to this paper, proofs (2010), http://www.cs.unibo.it/~sangio/
Demangeon, R., Hirschkoff, D., Sangiorgi, D.: A Method for Termination in a λ-calculus with References (2010), http://www.cs.unibo.it/~sangio/
Deng, Y., Sangiorgi, D.: Ensuring Termination by Typability. Information and Computation 204(7), 1045–1082 (2006)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1988)
Pierce, B.C., Turner, D.N.: Pict: a programming language based on the pi-calculus. In: Proof, Language, and Interaction, pp. 455–494. The MIT Press, Cambridge (2000)
Sangiorgi, D.: Termination of Processes. Math. Structures in Comput. Sci. 16(1), 1–39 (2006)
Sangiorgi, D., Walker, D.: The π-calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Turner, N.D.: The polymorphic pi-calculus: Theory and Implementation. PhD thesis, Department of Computer Science, University of Edinburgh (1996)
Yoshida, N., Berger, M., Honda, K.: 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
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Demangeon, R., Hirschkoff, D., Sangiorgi, D. (2010). Termination in Impure Concurrent Languages . In: Gastin, P., Laroussinie, F. (eds) CONCUR 2010 - Concurrency Theory. CONCUR 2010. Lecture Notes in Computer Science, vol 6269. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15375-4_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-15375-4_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15374-7
Online ISBN: 978-3-642-15375-4
eBook Packages: Computer ScienceComputer Science (R0)