Control effects as a modality
Research output: Contribution to journal › Article
Colleges, School and Institutes
We combine ideas from types for continuations, effect systems and monads in a very simple setting by defining a version of classical propositional logic in which double-negation elimination is combined with a modality. The modality corresponds to control effects, and it includes a form of effect masking. Erasing the modality from formulas gives classical logic. On the other hand, the logic is conservative over intuitionistic logic.
|Number of pages||10|
|Journal||Journal of Functional Programming|
|Early online date||6 Aug 2008|
|Publication status||Published - 1 Jan 2009|