The idea of costack may provide a term syntax for sequent calculus.

[xieyuheng]

I think the idea of costack may provide a term syntax for sequent calculus.

For example, in "Proofs and Types", 1989, Girard said:

As we have said, the syntactic point of view shows up some profound
symmetries of Logic. Gentzen’s sequent calculus does this in a
particularly satisfying manner. Unfortunately, the computational
significance is somewhat obscured by syntactic complications that,
although certainly immaterial, have never really been overcome.
That is why we present Prawitz’ natural deduction before we deal
with sequent calculus.

What "have never really been overcome" is to design a term syntax for sequent calculus
-- i.e. syntax for writing proofs, just like
using lambda terms for writing proofs in natural deduction.

We know that, in sequent calculus:

• The antecedent is a conjunction,
  which can obviously be handled
  by a simple stack-based concatenative language.

• But the succedent is a disjunction,
  previously nobody can handle this well,
  but your discovery of costack might help solve this problem.