Control effects as a modality

Research output: Contribution to journalArticle

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.


Original languageEnglish
Pages (from-to)17-26
Number of pages10
JournalJournal of Functional Programming
Issue number01
Early online date6 Aug 2008
Publication statusPublished - 1 Jan 2009