Abstract
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.
Original language | English |
---|---|
Pages (from-to) | 17-26 |
Number of pages | 10 |
Journal | Journal of Functional Programming |
Volume | 19 |
Issue number | 01 |
Early online date | 6 Aug 2008 |
DOIs | |
Publication status | Published - 1 Jan 2009 |