Output details

Control effects as a modality

<08>Under the Curry-Howard correspondence, types in programming languages can be read as propositions in logic. This connection has been particularly fruitful for control operators, since they correspond to classical logic. Another connection exists between effect systems and modal logics. However, none of these addresses the masking of effects, where the rest of the program cannot observe effects that are only visible in a part of the program. In this paper, we give a new logical reading to the notion of effect masking for control operators by a combination of modal and classical logic.