Call-with-current-continuation - Relation To Non-constructive Logic

Relation To Non-constructive Logic

The Curry-Howard correspondence between proofs and programs relates call/cc to Peirce's law, which extends intuitionistic logic to non-constructive, classical logic: ((α → β) → α) → α. Here, ((α → β) → α) is the type of the function f, which can either return a value of type α directly or apply an argument to the continuation of type (α → β). Since the existing context is deleted when the continuation is applied, the type β is never used and may be taken to be ⊥.

The principle of double negative elimination ((α → ⊥) → ⊥) → α is comparable to a variant of call-cc which expects its argument f to always evaluate the current continuation without normally returning a value.

Embeddings of classical logic into intuitionistic logic are related to continuation passing style translation.