Control effects as a modality

Hayo Thielecke

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)
223 Downloads (Pure)


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

Cite this