Skip to main content
SpringerLink
Log in

Shifting the Blame

A Blame Calculus with Delimited Control

  • Conference paper
  • First Online:
Book cover Programming Languages and Systems (APLAS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9458))

Included in the following conference series:

  • 677 Accesses

Abstract

We study integration of static and dynamic typing in the presence of delimited-control operators. In a program where typed and untyped parts coexist, the run-time system has to monitor the flow of values between these parts and abort program execution if invalid values are passed. However, control operators, which enable us to implement useful control effects, make such monitoring tricky; in fact, it is known that, with a standard approach, certain communications between typed and untyped parts can be overlooked.

We propose a new cast-based mechanism to monitor all communications between typed and untyped parts for a language with control operators shift and reset. We extend a blame calculus with shift/reset to give its semantics (operational semantics and CPS transformation) and prove two important correctness properties of the proposed mechanism: Blame Theorem and soundness of the CPS transformation.

S. Ueda—Current affiliation: Works Applications Co., Ltd.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Precisely speaking, even untyped programs need casts to use values of the dynamic type as functions, integers, etc., but we omit them to avoid the clutter.

References

  1. Ahmed, A., Findler, R.B., Siek, J.G., Wadler, P.: Blame for all. In: Proceedings of ACM POPL, pp. 201–214 (2011)

    Google Scholar 

  2. Asai, K., Kameyama, Y.: Polymorphic delimited continuations. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 239–254. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Asai, K., Kameyama, Y.: Polymorphic delimited continuations. CS-TR-07-10, Department of Computer Science, University of Tsukuba (2007)

    Google Scholar 

  4. Bonnaire-Sargeant, A., Davies, R., Tobin-Hochstadt, S.: Practical optional types for Clojure (unpublishded draft)

    Google Scholar 

  5. Danvy, O., Filinski, A.: A functional abstraction of typed contexts. 89/12, DIKU, University of Copenhagen (1989)

    Google Scholar 

  6. Danvy, O., Filinski, A.: Abstracting control. In: LISP and Functional Programming, pp. 151–160 (1990)

    Google Scholar 

  7. Dariusz Biernacki, O.D., Millikin, K.: A dynamic continuation-passing style for dynamic delimited continuations. Research Series RS-06-15, BRICS, DAIMI (2006)

    Google Scholar 

  8. Dimoulas, C., Tobin-Hochstadt, S., Felleisen, M.: Complete monitors for behavioral contracts. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 214–233. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  9. Dybvig, R.K., Jones, S.L.P., Sabry, A.: A monadic framework for delimited continuations. J. Funct. Program. 17(6), 687–730 (2007)

    Google Scholar 

  10. Felleisen, M.: The theory and practice of first-class prompts. In: Proceedings of ACM POPL, pp. 180–190 (1988)

    Google Scholar 

  11. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103(2), 235–271 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  12. Filinski, A.: Representing monads. In: Proceedings of ACM POPL, pp. 446–457 (1994)

    Google Scholar 

  13. Findler, R.B., Felleisen, M.: Contracts for higher-order functions. In: Proceedings of ACM ICFP, pp. 48–59 (2002)

    Google Scholar 

  14. Flanagan, C.: Hybrid type checking. In: Proceedings of ACM POPL, pp. 245–256 (2006)

    Google Scholar 

  15. Flatt, M., Yu, G., Findler, R.B., Felleisen, M.: Adding delimited and composable control to a production programming environment. In: Proceedings of ACM ICFP, pp. 165–176 (2007)

    Google Scholar 

  16. Herman, D., Tomb, A., Flanagan, C.: Space-efficient gradual typing. In: Trends in Functional Programming (2007)

    Google Scholar 

  17. Kameyama, Y., Kiselyov, O., Shan, C.: Shifting the stage: staging with delimited control. In: Proceedings of ACM PEPM, pp. 111–120 (2009)

    Google Scholar 

  18. Kameyama, Y., Yonezawa, T.: Typed dynamic control operators for delimited continuations. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 239–254. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  19. Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of ACM Annual Conference, pp. 717–740 (1972)

    Google Scholar 

  20. Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp Symbolic Comput. 6(3–4), 289–360 (1993)

    Article  Google Scholar 

  21. Shan, C.: Shift to control. In: Scheme and Functional Programming Workshop, pp. 99–107 (2004)

    Google Scholar 

  22. Siek, J.G., Taha, W.: Gradual typing for functional languages. In: Scheme and Functional Programming Workshop, pp. 81–92 (2006)

    Google Scholar 

  23. Siek, J.G., Taha, W.: Gradual typing for objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2–27. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Siek, J.G., Wadler, P.: Threesomes, with and without blame. In: Proceedings of ACM POPL, pp. 365–376 (2010)

    Google Scholar 

  25. Sitaram, D.: Handling control. In: Proceedings of ACM PLDI, pp. 147–155 (1993)

    Google Scholar 

  26. Takikawa, A., Strickland, T.S., Tobin-Hochstadt, S.: Constraining delimited control with contracts. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 229–248. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  27. Tobin-Hochstadt, S., Felleisen, M.: Interlanguage migration: from scripts to programs. In: Dynamic Language Symposium, pp. 964–974 (2006)

    Google Scholar 

  28. Tobin-Hochstadt, S., Felleisen, M.: The design and implementation of typed scheme. In: Proceedings of ACM POPL, pp. 395–406 (2008)

    Google Scholar 

  29. Vitousek, M.M., Kent, A.M., Siek, J.G., Baker, J.: Design and evaluation of gradual typing for Python. In: Dynamic Language Symposium, pp. 45–56 (2014)

    Google Scholar 

  30. Wadler, P., Findler, R.B.: Well-typed programs can’t be blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1–16. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  31. Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

We would like to thank Matthias Felleisen, Robby Findler, Philip Wadler, and anonymous reviewers of APLAS 2015 for valuable comments. This work was supported in part by Grant-in-Aid for Scientific Research (B) No. 25280024 from MEXT of Japan. The title is derived from that of a paper by Kameyama, Kiselyov, and Shan [17].

Author information

Authors and Affiliations

  1. Graduate School of Informatics, Kyoto University, Kyoto, Japan

    Taro Sekiyama, Soichiro Ueda & Atsushi Igarashi

Authors
  1. Taro Sekiyama
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Soichiro Ueda
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Atsushi Igarashi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Taro Sekiyama .

Editor information

Editors and Affiliations

  1. Univ. of Science and Technology of China, Hefei, Anhui, China

    Xinyu Feng

  2. Pohang Univ. of Science and Technology, Nam-Gu, Pohang, Korea (Republic of)

    Sungwoo Park

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Sekiyama, T., Ueda, S., Igarashi, A. (2015). Shifting the Blame. In: Feng, X., Park, S. (eds) Programming Languages and Systems. APLAS 2015. Lecture Notes in Computer Science(), vol 9458. Springer, Cham. https://doi.org/10.1007/978-3-319-26529-2_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-26529-2_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-26528-5

  • Online ISBN: 978-3-319-26529-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation