Abstract
Most programming languages provide abstractions for non-local control flow and access to the stack by using continuations, coroutines, or generators. However, their unrestricted use breaks the local reasoning capability of a programmer. Gradual typing exacerbates this problem because typed and untyped code co-exist. We present a contract system capable of protecting code from control flow and stack manipulations by unknown components. We use these contracts to support a gradual type system, and we prove that the resulting system cannot blame typed components for errors.
Supported in part by NSF CRI-0855140, SHF-1064922, CCF-0915978, the Mozilla Foundation, and the DARPA CRASH program.
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
Ahmed, A., Findler, R.B., Siek, J.G., Wadler, P.: Blame for All. In: Proc. ACM Sym. Principles of Programming Languages, pp. 201–214 (2011)
Asai, K., Kameyama, Y.: Polymorphic Delimited Continuations. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 239–254. Springer, Heidelberg (2007)
Clements, J.: Portable and High-level Access to the Stack with Continuation Marks. PhD dissertation, Northeastern University (2006)
Clements, J., Flatt, M., Felleisen, M.: Modeling an Algebraic Stepper. In: Proc. European Sym. on Programming, pp. 320–334 (2001)
Clements, J., Sundaram, A., Herman, D.: Implementing Continuation Marks in Javascript. In: Proc. Wksp. Scheme and Functional Programming (2008)
Danvy, O., Filinski, A.: Abstracting Control. In: Proc. LISP and Functional Programming, pp. 151–160 (1990)
Dimoulas, C.: Foundations for Behavioral Higher-Order Contracts. PhD dissertation, Northeastern University (2012)
Dimoulas, C., Felleisen, M.: On Contract Satisfaction in a Higher-Order World. Trans. Programming Languages and Systems 33(5), 16:1–16:29 (2011)
Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M.: Complete Monitors for Behavioral Contracts. In: Proc. European Sym. on Programming, pp. 214–233 (2012)
Draves, R.P.: Control Transfer in Operating System Kernels. PhD dissertation, Carnegie Mellon University (1994)
Dybvig, K., Peyton-Jones, S., Sabry, A.: A Monadic Framework for Delimited Continuations. J. Functional Programming 17(6), 687–730 (2007)
Felleisen, M.: The Theory and Practice of First-Class Prompts. In: Proc. ACM Sym. Principles of Programming Languages, pp. 180–190 (1988)
Felleisen, M.: On the Expressive Power of Programming Languages. Science of Computer Programming 17(1-3), 35–75 (1991)
Findler, R.B., Felleisen, M.: Contracts for Higher-Order Functions. In: Proc. ACM Intl. Conf. Functional Programming, pp. 48–59 (2002)
Flatt, M., PLT: Reference: Racket. PLT Inc., PLT-TR-2010-1 (2010), http://racket-lang.org/tr1/
Flatt, M., Yu, G., Findler, R.B., Felleisen, M.: Adding Delimited and Composable Control to a Production Programming Environment. In: Proc. ACM Intl. Conf. Functional Programming, pp. 165–176 (2007)
Free Software Foundation. Guile Reference Manual: Prompts (2012), http://www.gnu.org/software/guile/manual/html_node/Prompts.html
Gunter, C.A., Didier, R., Riecke, J.G.: A Generalization of Exceptions and Control in ML-like Languages. In: Proc. ACM Intl. Conf. Functional Programming Languages and Computer Architecture, pp. 12–23 (1995)
Hieb, R., Kent Dybvig, R., Anderson, C.W.: Subcontinuations. In: LISP and Symbolic Computation, pp. 83–110 (1994)
James, R.P., Sabry, A.: Yield: Mainstream Delimited Continuations. In: Proc. Theory and Practice of Delimited Continuations, pp. 20–32 (2011)
Kiselyov, O., Shan, C.-C.: A Substructural Type System for Delimited Continuations. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 223–239. Springer, Heidelberg (2007)
Kiselyov, O., Shan, C.-C., Sabry, A.: Delimited Dynamic Binding. In: Proc. ACM Intl. Conf. Functional Programming, pp. 26–37 (2006)
Pettyjohn, G., Clements, J., Marshall, J., Krishnamurthi, S., Felleisen, M.: Continuations from Generalized Stack Inspection. In: Proc. ACM Intl. Conf. Functional Programming, pp. 216–227 (2005)
Siek, J.G., Taha, W.: Gradual Typing for Functional Languages. In: Proc. Wksp. Scheme and Functional Programming (2006)
Siek, J.G., Taha, W.: Gradual Typing for Objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2–27. Springer, Heidelberg (2007)
Sitaram, D.: Handling Control. In: Proc. ACM Conf. Programming Language Design and Implementation, pp. 147–155 (1993)
Sitaram, D., Felleisen, M.: Control Delimiters and their Hierarchies. In: LISP and Symbolic Computation, pp. 67–99 (1990)
Stephen Strickland, T., Tobin-Hochstadt, S., Findler, R.B., Flatt, M.: Chaperones and Impersonators: Run-time Support for Reasonable Interposition. In: Proc. ACM Conf. Object-Oriented Programming, Systems, Languages and Applications (2012)
Takikawa, A., Stephen Strickland, T., Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M.: Gradual Typing for First-Class Classes. In: Proc. ACM Conf. Object-Oriented Programming, Systems, Languages and Applications (2012)
Takikawa, A., Stephen Strickland, T., Tobin-Hochstadt, S.: Constraining Delimited Control with Contracts. Northeastern University, NU-CCIS-13-01 (2013)
Tobin-Hochstadt, S., Felleisen, M.: Interlanguage Migration: from Scripts to Programs. In: Proc. Dynamic Languages Symposium, pp. 964–974 (2006)
Tobin-Hochstadt, S., Felleisen, M.: The Design and Implementation of Typed Scheme. In: Proc. ACM Sym. Principles of Programming Languages, pp. 395–406 (2008)
Tucker, D.B., Krishnamurthi, S.: Pointcuts and Advice in Higher-Order Languages. In: Proc. Intl. Conf. on Aspect-Oriented Software Development, pp. 158–167 (2003)
Wadler, P., Findler, R.B.: Well-typed Programs Can’t be Blamed. In: Proc. European Sym. on Programming, pp. 1–15 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Takikawa, A., Strickland, T.S., Tobin-Hochstadt, S. (2013). Constraining Delimited Control with Contracts. In: Felleisen, M., Gardner, P. (eds) Programming Languages and Systems. ESOP 2013. Lecture Notes in Computer Science, vol 7792. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37036-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-37036-6_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37035-9
Online ISBN: 978-3-642-37036-6
eBook Packages: Computer ScienceComputer Science (R0)