MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

To answer your question about representing sequent calculi proofs in a computer, you need to look at the Curry-Howard isomorphism. Formula in a sequent are annotated with terms and the sequent calculus for intuitionistic logic resembles the type rules for the typed lambda calculus. If you want to manipulate this, then you need to record the assumptions (left-hand side of the turnstyle $\vdash$), which corresponds to recording the types of free variables. Then the right-hand side is a $\lambda$-term (describing the proof) and its type (the formula proven).

There's a vast amount of literature about this. For example the The reference you probably want is A $\lambda$-calculus structure isomorphic to sequent calculus structure by Hugo Herbelin. The book by Morten Heine B. Sørensen and Pawel Urzyczyn is an extensive study of the topic. This kind of encoding is at the heart of proof assistants such as Coq.

Other possible correspondences include Sequent calculus ~ Abstract Machine. See Sequent calculi and abstract machines by Zena M. Ariola, Aaron Bohannon, Amr Sabry, ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 31 , Issue 4 (May 2009). Or more generally, and perhaps more loosely, Sequent calculus ~ Operational Semantics. You also have proofs ~ processes, as explored by Abramsky and Saraswat, the latter in the context of concurrent constraint programming.

7 Refined text a little.

To answer the additional your question you added, about representing sequent calculi proofs in a computer, you need to look at the Curry-Howard isomorphism. Formula in a sequent are annotated with terms and the sequent calculus for intuitionistic logic resembles the type rules for the typed lambda calculus. If you want to manipulate this, then you need to record the assumptions (left-hand side of the turnstyle $\vdash$), which corresponds to recording the types of free variables. Then the right-hand side is a $\lambda$-term (describing the proof) and its type (the formula proven).

There's a vast amount of literature about this. For example the book by Morten Heine B. Sørensen and Pawel Urzyczyn. This kind of encoding is at the heart of proof assistants such as Coq.

Other possible answers correspondences include Sequent calculus ~ Abstract Machine. See Sequent calculi and abstract machines by Zena M. Ariola, Aaron Bohannon, Amr Sabry, ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 31 , Issue 4 (May 2009). Or more generally, and perhaps more loosely, Sequent calculus ~ Operational Semantics. You also have proofs ~ processes, as explored by Abramsky and Saraswat, the latter in the context of concurrent constraint programming.

6 Reshuffled the text to better reflect the changes in the question.

One possible answer is Sequent calculus ~ Abstract Machine. See Sequent calculi and abstract machines by Zena M. Ariola, Aaron Bohannon, Amr Sabry, ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 31 , Issue 4 (May 2009).

More generally, and perhaps more loosely, Sequent calculus ~ Operational Semantics.

Alternatively, you have proofs ~ processes, as explored by Abramsky and Saraswat, the latter in the context of concurrent constraint programming.

To answer the additional question you added, about representing sequent calculi proofs in a computer, you need to look at the Curry-Howard isomorphism. Formula in a sequent are annotated with terms and the sequent calculus for intuitionistic logic resembles the type rules for the typed lambda calculus. If you want to manipulate this, then you need to record the assumptions (left-hand side of the turnstyle $\vdash$), which corresponds to recording the types of free variables. Then the right-hand side is a $\lambda$-term (describing the proof) and its type (the formula proven).

There's a vast amount of literature about this. For example the book by Morten Heine B. Sørensen and Pawel Urzyczyn. This kind of encoding is at the heart of proof assistants such as Coq.

Other possible answers include Sequent calculus ~ Abstract Machine. See Sequent calculi and abstract machines by Zena M. Ariola, Aaron Bohannon, Amr Sabry, ACM Transactions on Programming Languages and Systems (TOPLAS) Volume 31 , Issue 4 (May 2009). Or more generally, and perhaps more loosely, Sequent calculus ~ Operational Semantics. You also have proofs ~ processes, as explored by Abramsky and Saraswat, the latter in the context of concurrent constraint programming.

5 added 962 characters in body
4 added 173 characters in body