Skip to main content
11 votes
Accepted

How do continuations represent negations (under the Curry–Howard correspondence)?

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type ...
Dan Doel's user avatar
  • 1,021
5 votes
Accepted

What's the logical counterpart to jumps with arguments on CPS terms?

Such a logic of continuations (or a syntax of continuation that arose from logical considerations) would be Laurent's “polarised linear logic” (LLP): Olivier Laurent, Étude de la polarisation en ...
gadmm's user avatar
  • 307
3 votes

What's the logical counterpart to jumps with arguments on CPS terms?

For me, what is going on is reasonably standard: You have $c$ with free variables $(x_i : \tau_i)_i$, and you replace it with $c[t_i/x_i]$ with the $(t_i)_i$ at types $(\tau_i)_i$; this is a standard ...
gasche's user avatar
  • 2,040
2 votes
Accepted

Can you regain the Church-Rosser property in languages with continuations?

A simple fix is to add call-by-value let-expressions$$\text{let } x := t\text{ in }u$$that evaluate $t$ to a value and then substitute it for $x$. Having these in the language allows to restrict $+$ ...
xavierm02's user avatar
  • 556
1 vote

What's the logical counterpart to jumps with arguments on CPS terms?

You may be interested in the Kappa calculus which has no higher order maps and broadly corresponds to Cartesian categories. You might also want to look into co-intuitionistic logic which has "...
Ms. Molly Stewart-Gallus's user avatar
1 vote

How do continuations represent negations (under the Curry–Howard correspondence)?

Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for any formula $X$, the subset of formulae $\overline{A} = A → X$ is a reverse-mapping of ...
NinjaDarth's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible