Abstract
This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. These technical results establish the foundation of polymorphic delimited continuations.
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
Asai, K.: Logical Relations for Call-by-value Delimited Continuations. Trends in Functional Programming 6, 63–78 (2007)
Asai, K.: On Typing Delimited Continuations: Three New Solutions to the Printf Problem. See http://pllab.is.ocha.ac.jp/~asai/papers/ (submitted, 2007)
Asai, K., Kameyama, Y.: Polymorphic Delimited Continuations. Technical Report CS-TR-07-10, Dept. of Computer Science, University of Tsukuba (September 2007)
Danvy, O.: An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark (2006)
Danvy, O., Filinski, A.: A Functional Abstraction of Typed Contexts. Technical Report 89/12, DIKU, University of Copenhagen (July 1989)
Danvy, O., Filinski, A.: Abstracting Control. In: Proc. 1990 ACM Conference on Lisp and Functional Programming, pp. 151–160 (1990)
Danvy, O., Filinski, A.: Representing Control: a Study of the CPS Transformation. Mathematical Structures in Computer Science 2(4), 361–391 (1992)
Filinski, A.: Representing Monads. In: POPL, pp. 446–457 (1994)
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press, Cambridge (1989)
Gunter, C.A., Remy, D., Riecke, J.G.: A Generalization of Exceptions and Control in ML-Like Languages. In: FPCA, pp. 12–23 (1995)
Harper, R., Duba, B.F., MacQueen, D.: Typing First-Class Continuations in ML. J. Funct. Program. 3(4), 465–484 (1993)
Harper, R., Lillibridge, M.: Explicit polymorphism and CPS conversion. In: POPL, pp. 206–219 (1993)
Hasegawa, M.: Relational parametricity and control. Logical Methods in Computer Science 2(3) (2006)
Kiselyov, O., Shan, C.-c., Sabry, A.: Delimited dynamic binding. In: ICFP, pp. 26–37 (2006)
Leroy, X.: Polymorphism by name for references and continuations. In: POPL, pp. 220–231 (1993)
Mogelberg, R.E., Simpson, A.: Relational parametricity for computational effects. In: LICS (2007)
Strachey, C.: Fundamental concepts in programming languages. International Summer School in Computer Programming, Copenhagen, Denmark (August 1967)
Thielecke, H.: From Control Effects to Typed Continuation Passing. In: POPL, pp. 139–149. ACM Press, New York (2003)
Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1–34 (1990)
Wright, A.K.: Simple imperative polymorphism. Lisp and Symbolic Computation 8(4), 343–355 (1995)
Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asai, K., Kameyama, Y. (2007). Polymorphic Delimited Continuations. In: Shao, Z. (eds) Programming Languages and Systems. APLAS 2007. Lecture Notes in Computer Science, vol 4807. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76637-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-76637-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76636-0
Online ISBN: 978-3-540-76637-7
eBook Packages: Computer ScienceComputer Science (R0)