All Questions
Tagged with continuations curry-howard
3 questions
14
votes
3
answers
998
views
How do continuations represent negations (under the Curry–Howard correspondence)?
Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
- 243
8
votes
3
answers
776
views
What's the logical counterpart to jumps with arguments on CPS terms?
It's well known that the CPS (continuation-passing style) translation often employed in compilers corresponds to double negation translation under the Curry-Howard isomorphism. Though often the target ...
- 387
4
votes
0
answers
109
views
Description of the CPS transformation for the typed lambda-calculus
Is there somewhere a precise but hopefully readable account of how the CPS (=continuation-passing-style) transformation applies to the typed lambda-calculus? (Say, simply-typed with product and sum ...
- 851