|
Abstract:
First-class delimited continuations (aka "shift" and "reset") are control operators which provide programmers an access to fine control over programs. In the literature several types systems for them have been proposed, however, none of them are satisfactory from programmers'and/or theoreticians' viewpoint. To fill this gap, we propose a simple type (and effect) system for them, and show our type system enjoys all pleasant properties and can type most examples. We also connect our type system to constructive modal logic.
|