Editing Call-with-current-continuation (section)

== 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 empty type.

The principle of [[double negation 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.<ref name=ch-isomorphy>{{cite book|last1=Sørensen|first1=Morten Heine|last2=Urzyczyn|first2=Paweł|title=Lectures on the Curry-Howard isomorphism|date=2007|publisher=Elsevier|location=Boston, MA|isbn=978-0444520777|edition=1st|chapter=Classical Logic and Control Operators}}</ref>