Questions tagged [continuations]
The continuations tag has no usage guidance.
12 questions
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
7
votes
1
answer
214
views
Can you regain the Church-Rosser property in languages with continuations?
I'm aware that if you naively add continuations to a language, the Church-Rosser property no longer holds. For example, suppose we have some variant of the STLC with basic arithmetic and integer types....
- 81
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
2
votes
0
answers
108
views
"finally" for algebraic effects and handlers
In Java in addition to catch there is also finally, this is very important to make sure resources get cleaned up. I believe <...
- 701
3
votes
0
answers
197
views
Type System Of $\lambda\mu$-Calculus
reading this paper on CPS-tranformation from the $\lambda\mu$-calculus, I'm a bit confused about the type system presented:
Why second-order formulas in the types? Is this according to the Curry-...
- 139
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
0
votes
2
answers
653
views
reset and shift only one level deep (delimited continuations)? [closed]
I'm looking at the following tutorial on delimited (or composable) continuations:
http://community.schemewiki.org/?composable-continuations-tutorial
The author(s) propose the following "rewrite ...
- 117
8
votes
1
answer
528
views
What is the formal definitions of the reduction related to the "call/cc" (call with the current continuation) operator?
In lambda calculus or in combinatory logic we formally define reduction/expansion rules for terms (and in their typed variants reductions must preserve the type). Then we can talk about properties of ...
- 2,611
0
votes
1
answer
80
views
Seeking for a game for modelling a problem using game thoery [closed]
I have a problem which I want to formulate it as a game, using game theory. In this problem there is several agents, we can consider the agents as the employees of different offices, these agents have ...
- 1
12
votes
0
answers
167
views
Are the types that show monads are more powerful than continuations revealing something of fundamental importance?
In 1992 in the paper Imperative Functional Programming, Simon Peyton Jones and Philip Wadler write:
So monads are more powerful than continuations, but only because of the types! It is not clear ...
- 2,581
12
votes
2
answers
656
views
Continuation passing transform of binary functions
Recall the continuation passing transform (CPS transform) which takes $A$ to $\beta A \mathrel{{:}{=}} R^{R^A}$ (where $R$ is fixed) and $f : A \to B$ to $\beta f : \beta A \to \beta B$ defined by
$$\...
- 29.5k
4
votes
2
answers
394
views
Reversing the CPS transformation?
A quick Google search didn't turn up anything obvious, so I'm asking here.
Converting direct style programs to continuation-passing style is a well-studied program transformation. However, I'm ...
- 32.9k