# Tag Info

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 ...
• 1,021
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 ...
• 307

### 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 ...
• 2,040
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 $+$ ...
• 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 "...
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 ...
• 121

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