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 language of a CPS translation is the same as the source language, sometimes it's a specialized language which only allows terms in CPS form (i.e., there are no direct style functions anymore). See, e.g., this or this.

As an example, consider Thielecke's CPS-calculus, where commands are defined as either jumps or bindings:

$$b ::= x\langle\vec{x}\rangle\ |\ b\ \{\ x\langle\vec{x}\rangle = b\ \}$$

And one-hole contexts (commands with holes) are defined as follow:

$$C ::= [-]\ |\ C \ \{\ x\langle\vec{x}\rangle = b\ \}\ |\ b\ \{\ x\langle\vec{x}\rangle = C\ \}$$

If we try to see these languages under the Curry-Howard isomorphism, we don't have implication anymore, but rather we use negations and products alone. The typing rules for such languages demonstrate we're trying to derive a contradiction:

$$\frac{\color{orange}{\Gamma\vdash} k{:}\ \color{orange}{\neg\vec{\tau}}\quad\quad\color{orange}{\Gamma\vdash}\vec{x}{:}\ \color{orange}{\vec{\tau}}}{\color{orange}{\Gamma\vdash} k\langle\vec{x}\rangle}(J)$$

$$\frac{\color{orange}{\Gamma,}k{:}\ \color{orange}{\neg\vec{\tau}\vdash} b\quad\quad\color{orange}{\Gamma,}\vec{x}{:}\ \color{orange}{\vec{\tau}\vdash} c}{\color{orange}{\Gamma\vdash} b\ \{\ k\langle\vec{x}\rangle=c\ \}}(B)$$

(Note that these look similar to the (AXIOM) and (CUT) rules from linear logic, though on the other side of the sequent: we have a conjunction rather than a disjunction.)

Reduction rules in intermediate languages such as the ones above allow jumps to be performed to bound continuations, immediately replacing arguments (hence the name "jump with arguments" sometimes employed). For the CPS-calculus, this can be represented by the following reduction rule:

$$\frac{}{C[\color{blue}{k\langle \vec{x}\rangle}]\ \{\ k\langle\color{red}{\vec{y}}\rangle=\color{red}c\ \} \longrightarrow C[\color{red}{c[\color{blue}{\vec{x}}/\vec{y}]}]\ \{\ k\langle\color{red}{\vec{y}}\rangle=\color{red}c\ \}}$$

$$\frac{a\longrightarrow b}{C[a]\longrightarrow C[b]}$$

...though similar languages have similar notions of jump. I'm not totally sure, but I believe that the reduction rule would corresponde to a cut inference rule similar to the following (quickly sketched):

...where we're allowed to copy a bound proof tree and replace the jump subtree with it (in the example above, replacing subtree a with a copy of subtree b, though with a different context).

I'm interested on how such an intermediate language could be seen by the Curry-Howard isomorphism. So, my actual question is twofold:

1. Has a similar implication-free subset of some logic (e.g., propositional logic) been studied somewhere? I mean, has a "logic without implication" been proposed?
2. What is the equivalent of a jump with arguments in logic? Assuming the cut rule I sketched above is correct (and it corresponds to the reduction rule), has something similar to it appeared elsewhere?

Asked by user51841 (253 )
Jan 12, 2022 at 05:35