Sciweavers

Share
APLAS
2015
ACM

Shifting the Blame - A Blame Calculus with Delimited Control

4 years 3 months ago
Shifting the Blame - A Blame Calculus with Delimited Control
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.
Taro Sekiyama, Soichiro Ueda, Atsushi Igarashi
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where APLAS
Authors Taro Sekiyama, Soichiro Ueda, Atsushi Igarashi
Comments (0)
books