Abstract
Type and effect systems are a tool to analyse statically the behaviour of programs with effects. We present a proof based on the so called reducibility candidates that a suitable stratification of the type and effect system entails the termination of the typable programs. The proof technique covers a simply typed, multi-threaded, call-by-value lambda-calculus, equipped with a variety of scheduling (preemptive, cooperative) and interaction mechanisms (references, channels, signals).
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. Report ArXiv:0904.2076
Amadio, R., Curien, P.-L.: Domains and Lambda Calculi. Cambridge University Press, Cambridge
Amadio, R., Dabrowski, F.: Feasible reactivity in a synchronous π-calculus. In: Proc. ACM Principles and Practice of Declarative Programming, pp. 221–230 (2007)
Boudol, G.: Typing termination in a higher-order concurrent imperative language. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 272–286. Springer, Heidelberg (2007)
Berry, G., Gonthier, G.: The Esterel synchronous programming language. Science of computer programming 19(2), 87–152 (1992)
Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Information and Computation 204(7), 1045–1082 (2006)
Gallier, J.: On Girard’s Candidats de Reductibilité. In: Odifreddi (ed.) Logic and Computer Science, pp. 123–203. Academic Press, London (1990)
Hennessy, M., Regan, T.: A process algebra of timed systems. Information and Computation 117(2), 221–239 (1995)
Lucassen, J., Gifford, D.: Polymorphic effect systems. In: Proc. ACM-POPL (1988)
Sangiorgi, D.: Termination of processes. Math. Struct. in Comp. Sci. 16, 1–39 (2006)
Tofte, M., Talpin, J.-P.: Region-based memory management. Information and Computation 132(2), 109–176 (1997)
Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the π-calculus. Information and Computation 191(2), 145–202 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amadio, R.M. (2009). On Stratified Regions. In: Hu, Z. (eds) Programming Languages and Systems. APLAS 2009. Lecture Notes in Computer Science, vol 5904. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10672-9_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-10672-9_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10671-2
Online ISBN: 978-3-642-10672-9
eBook Packages: Computer ScienceComputer Science (R0)