Continuation manipulation vs. intuitionistic/linear implication

Using intuitionistic implication (actullay it should be -: but let's forget this for a moment) we can write in BinProlog: 

    insert(X, Xs, Ys) :- 
        paste(X) => ins(Xs, Ys). 

    ins(Ys, [X|Ys]) :- paste(X).
    ins([Y|Ys], [Y|Zs]):- ins(Ys, Zs).

used
to nondeterministically insert an element in a list, the unit clause paste(X) is available only within the scope of the derivation for ins. This gives: 

?- insert(a,[1,2,3],X).
X=[a,1,2,3];

X=[1,a,2,3];

X=[1,2,a,3];

X=[1,2,3,a]

With respect to the corresponding Prolog program we are working with a simpler formulation in which the element to be inserted does not have to percolate as dead weight throughout each step of the computation, only to be used in the very last step. We instead clearly isolate it in a global-value manner, within a unit clause which will only be consulted when needed, and which will disappear afterwards.

Now, let us imagine we are given the ability to write part of a proof state context, i.e., to indicate in a rule's left-hand side not only the predicate which should match a goal atom to be replaced by the rule's body, but also which other goal atom(s) should surround the targeted one in order for the rule to be applicable.

Given this, we could write, using BinProlog's @@ (which gives in its second argument the current continuation) a program for insert/3 which strikingly resembles the intuitionistic implication based program given above: 

insert(X,Xs,Ys):-ins(Xs,Ys),paste(X).

ins(Ys,[X|Ys]) @@ paste(X).
ins([Y|Ys],[Y|Zs]):-ins(Ys,Zs).

Note
that the element to be inserted is not passed to the recursive clause of the predicate ins/2 (which becomes therefore simpler), while the unit clause of the predicate ins/2 will communicate directly with insert/3 which will directly `paste' the appropriate argument in the continuation.

In this formulation, the element to be inserted is first given as right-hand side context of the simpler predicate ins/2, and this predicate's first clause consults the context paste(X) only when it is time to place it within the output list, i.e. when the fact ins(Ys,[X|Ys]),paste(X) is reached.

Thus for this example, we can also obtain the expressive power of intuitionistic/linear implication by this kind of (much more efficient) direct manipulation of BinProlog's first order continuations.