2 subformula property

To add to Neel's response, you can't get a more concrete answer unless you clarify what you mean by "sequent calculus". If you mean Gentzen's original systems LK or LJ, then the answer is simply that there is no independently discovered/motivated computational system. (Remember that Gentzen's original motivation for introducing sequent calculus was as a tool for studying provability, and natural deduction as a tool for studying proofs.) Different operational interpretations have been associated with sequent calculus by departing from these original systems (or just by being satisfied with a looser "correspondence"), but then the questions are 1. whether you can really call these systems "sequent calculus" (what mathematical properties are invariant?), and 2. whether it really matters that you do?

On the other hand, there are still many aspects of proofs-as-programs that are not understood---as Neel and supercooldave mentioned, pattern-matching and operational semantics are examples---and people have tried to gain a handle on these by studying ideas from sequent calculus and from refinements of sequent calculus.

For example, one important idea from sequent calculus is the "subformula property", that a proof of a formula only needs to mention its subformulas. In natural deduction this property is broken for connectives like disjunction. The connection between focusing proofs and pattern-matching that Neel mentioned can be understood as a way of regaining this normal form property for programs with sum types.

1

To add to Neel's response, you can't get a more concrete answer unless you clarify what you mean by "sequent calculus". If you mean Gentzen's original systems LK or LJ, then the answer is simply that there is no independently discovered/motivated computational system. (Remember that Gentzen's original motivation for introducing sequent calculus was as a tool for studying provability, and natural deduction as a tool for studying proofs.) Different operational interpretations have been associated with sequent calculus by departing from these original systems (or just by being satisfied with a looser "correspondence"), but then the questions are 1. whether you can really call these systems "sequent calculus" (what mathematical properties are invariant?), and 2. whether it really matters that you do?

On the other hand, there are still many aspects of proofs-as-programs that are not understood---as Neel and supercooldave mentioned, pattern-matching and operational semantics are examples---and people have tried to gain a handle on these by studying ideas from sequent calculus and from refinements of sequent calculus.