Article

Constraining delimited control with contracts

Authors:

Asumu Takikawa,

T. Stephen Strickland,

Sam Tobin-HochstadtAuthors Info & Claims

ESOP'13: Proceedings of the 22nd European conference on Programming Languages and Systems

Pages 229 - 248

https://doi.org/10.1007/978-3-642-37036-6_14

Published: 16 March 2013 Publication History

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.

References

[1]

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)

Digital Library

[2]

Asai, K., Kameyama, Y.: Polymorphic Delimited Continuations. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 239-254. Springer, Heidelberg (2007)

Digital Library

[3]

Clements, J.: Portable and High-level Access to the Stack with Continuation Marks. PhD dissertation, Northeastern University (2006)

[4]

Clements, J., Flatt, M., Felleisen, M.: Modeling an Algebraic Stepper. In: Proc. European Sym. on Programming, pp. 320-334 (2001)

Digital Library

[5]

Clements, J., Sundaram, A., Herman, D.: Implementing Continuation Marks in Javascript. In: Proc. Wksp. Scheme and Functional Programming (2008)

[6]

Danvy, O., Filinski, A.: Abstracting Control. In: Proc. LISP and Functional Programming, pp. 151-160 (1990)

Digital Library

[7]

Dimoulas, C.: Foundations for Behavioral Higher-Order Contracts. PhD dissertation, Northeastern University (2012)

[8]

Dimoulas, C., Felleisen, M.: On Contract Satisfaction in a Higher-Order World. Trans. Programming Languages and Systems 33(5), 16:1-16:29 (2011)

Digital Library

[9]

Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M.: Complete Monitors for Behavioral Contracts. In: Proc. European Sym. on Programming, pp. 214-233 (2012)

Digital Library

[10]

Draves, R. P.: Control Transfer in Operating System Kernels. PhD dissertation, Carnegie Mellon University (1994)

[11]

Dybvig, K., Peyton-Jones, S., Sabry, A.: A Monadic Framework for Delimited Continuations. J. Functional Programming 17(6), 687-730 (2007)

Digital Library

[12]

Felleisen, M.: The Theory and Practice of First-Class Prompts. In: Proc. ACM Sym. Principles of Programming Languages, pp. 180-190 (1988)

Digital Library

[13]

Felleisen, M.: On the Expressive Power of Programming Languages. Science of Computer Programming 17(1-3), 35-75 (1991)

Digital Library

[14]

Findler, R. B., Felleisen, M.: Contracts for Higher-Order Functions. In: Proc. ACM Intl. Conf. Functional Programming, pp. 48-59 (2002)

Digital Library

[15]

Flatt, M., PLT: Reference: Racket. PLT Inc., PLT-TR-2010-1 (2010), http://racket-lang.org/tr1/

[16]

Flatt, M., Yu, G., Findler, R. B., Felleisen, M.: Adding Delimited and Composable Control to a Production Programming Environment. In: Proc. ACMIntl. Conf. Functional Programming, pp. 165-176 (2007)

Digital Library

[17]

Free Software Foundation. Guile Reference Manual: Prompts (2012), http://www.gnu.org/software/guile/manual/html_node/Prompts.html

[18]

Gunter, C. A., Didier, R., Riecke, J. G.: A Generalization of Exceptions and Control in MLlike Languages. In: Proc. ACM Intl. Conf. Functional Programming Languages and Computer Architecture, pp. 12-23 (1995)

Digital Library

[19]

Hieb, R., Kent Dybvig, R., Anderson, C. W.: Subcontinuations. In: LISP and Symbolic Computation, pp. 83-110 (1994)

Digital Library

[20]

James, R. P., Sabry, A.: Yield: Mainstream Delimited Continuations. In: Proc. Theory and Practice of Delimited Continuations, pp. 20-32 (2011)

[21]

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)

Digital Library

[22]

Kiselyov, O., Shan, C.-C., Sabry, A.: Delimited Dynamic Binding. In: Proc. ACM Intl. Conf. Functional Programming, pp. 26-37 (2006)

Digital Library

[23]

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)

Digital Library

[24]

Siek, J. G., Taha, W.: Gradual Typing for Functional Languages. In: Proc. Wksp. Scheme and Functional Programming (2006)

[25]

Siek, J. G., Taha, W.: Gradual Typing for Objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2-27. Springer, Heidelberg (2007)

Digital Library

[26]

Sitaram, D.: Handling Control. In: Proc. ACM Conf. Programming Language Design and Implementation, pp. 147-155 (1993)

Digital Library

[27]

Sitaram, D., Felleisen, M.: Control Delimiters and their Hierarchies. In: LISP and Symbolic Computation, pp. 67-99 (1990)

Digital Library

[28]

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)

Digital Library

[29]

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)

Digital Library

[30]

Takikawa, A., Stephen Strickland, T., Tobin-Hochstadt, S.: Constraining Delimited Control with Contracts. Northeastern University, NU-CCIS-13-01 (2013)

[31]

Tobin-Hochstadt, S., Felleisen, M.: Interlanguage Migration: from Scripts to Programs. In: Proc. Dynamic Languages Symposium, pp. 964-974 (2006)

Digital Library

[32]

Tobin-Hochstadt, S., Felleisen, M.: The Design and Implementation of Typed Scheme. In: Proc. ACM Sym. Principles of Programming Languages, pp. 395-406 (2008)

Digital Library

[33]

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)

Digital Library

[34]

Wadler, P., Findler, R. B.: Well-typed Programs Can't be Blamed. In: Proc. European Sym. on Programming, pp. 1-15 (2009)

Digital Library

Cited By

New MGiovannini ELicata D(2023)Gradual Typing for Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228607:OOPSLA2(1758-1786)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622860
Ikemori KCong YMasuhara H(2023)Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control OperatorsProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610616(1-13)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610616
Xie NCong YIkemori KLeijen D(2022)First-class names for effect handlersProceedings of the ACM on Programming Languages10.1145/35632896:OOPSLA2(30-59)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563289
Show More Cited By

Recommendations

Polymorphic delimited continuations
APLAS'07: Proceedings of the 5th Asian conference on Programming languages and systems

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 ...
Subtyping delimited continuations
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming

We present a type system with subtyping for first-class delimited continuations that generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit information about the types of contexts in the metacontext. We exploit this ...
Subtyping delimited continuations
ICFP '11

We present a type system with subtyping for first-class delimited continuations that generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit information about the types of contexts in the metacontext. We exploit this ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ESOP'13: Proceedings of the 22nd European conference on Programming Languages and Systems

March 2013

613 pages

ISBN:9783642370359

Editors:
Matthias Felleisen
College of Computer Science, Northeastern University, Boston, MA
,
Philippa Gardner
Department of Computing, Imperial College, London, MA, UK

Sponsors

Sapienza: Sapienza University of Rome

In-Cooperation

EAPLS: European Association for Programming Languages and Systems
EATCS: European Association for Theoretical Computer Science
European Association of Software Science and Technology

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 16 March 2013

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

New MGiovannini ELicata D(2023)Gradual Typing for Effect HandlersProceedings of the ACM on Programming Languages10.1145/36228607:OOPSLA2(1758-1786)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622860
Ikemori KCong YMasuhara H(2023)Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control OperatorsProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610616(1-13)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610616
Xie NCong YIkemori KLeijen D(2022)First-class names for effect handlersProceedings of the ACM on Programming Languages10.1145/35632896:OOPSLA2(30-59)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563289
Sekiyama TIgarashi A(2017)Stateful manifest contractsACM SIGPLAN Notices10.1145/3093333.300987552:1(530-544)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009875
Sekiyama TIgarashi ACastagna GGordon A(2017)Stateful manifest contractsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009875(530-544)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009875
Moore SDimoulas CFindler RFlatt MChong S(2016)Extensible access control with authorization contractsACM SIGPLAN Notices10.1145/3022671.298402151:10(214-233)Online publication date: 19-Oct-2016
https://dl.acm.org/doi/10.1145/3022671.2984021
Dimoulas CNew MFindler RFelleisen M(2016)Oh Lord, please don't let contracts be misunderstood (functional pearl)ACM SIGPLAN Notices10.1145/3022670.295193051:9(117-131)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951930
Moore SDimoulas CFindler RFlatt MChong SVisser ESmaragdakis Y(2016)Extensible access control with authorization contractsProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2983990.2984021(214-233)Online publication date: 19-Oct-2016
https://dl.acm.org/doi/10.1145/2983990.2984021
Dimoulas CNew MFindler RFelleisen MGarrigue JKeller GSumii E(2016)Oh Lord, please don't let contracts be misunderstood (functional pearl)Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951930(117-131)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951930
Findler R(2014)Behavioral software contractsACM SIGPLAN Notices10.1145/2692915.263285549:9(137-138)Online publication date: 19-Aug-2014
https://dl.acm.org/doi/10.1145/2692915.2632855
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents