show/hide this revision's text 5 edited body

intuitionistic logic ~ programming

natural deduction ~ lambda-calculus

Hilbert system ~ combinatory logic {S, K}

Gentzen system=sequent calculus ~ ?

What would you write in place of the question mark?

Update 0: Common mathematical tree notation for proofs is too cumbersome and redundant. I need a language as compact as e.g.:

data Proof = Apply Proof Proof | S | K {- Haskell, combinatory logic -}

Update 1: After following the links suggested by commentators I found this perfectly concrete and accessible article: "Hugo Herbelin. A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure." There, "?" language is named "the usual interpretation of LJ cut-free proofs by normal lambda-terms", i.e. is a subset made out of lambda-calculus.
show/hide this revision's text 4 answer

[solved] sequent calculus as programming language

intuitionistic logic ~ programming

natural deduction ~ lambda-calculus

Hilbert system ~ combinatory logic {S, K}

Gentzen system=sequent calculus ~ ?

What would you write in place of the question mark?"?" language is needed for representing proofs in computer. Maybe I can imagine it by myself, but it is so strange that no one asked this question before and therу is no standard name for this language.

Update 0: Common mathematical tree notation for proofs is too cumbersome and redundant. I need something a language as compact likeas e.g.:

data Proof = Apply Proof Proof | S | K {- Haskell, combinatory logic -}

Update 1: After following the links suggested by commentators I found this perfectly concrete and accessible article: "Hugo Herbelin. A Lambda-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure." There, "?" language is named "the usual interpretation of LJ cut-free proofs by normal lambda-terms", i.e. is a subset of lambda-calculus.
show/hide this revision's text 3 added 393 characters in body

intuitionistic logic ~ programming

natural deduction ~ lambda-calculus

Hilbert system ~ combinatory logic {S, K}

Gentzen system=sequent calculus ~ ?

What would you write in place of the question mark? "?" language is needed for representing proofs in computer. Maybe I can imagine it by myself, but it is so strange that no one asked this question before and therу is no standard name for this language. Common mathematical tree notation is too cumbersome and redundant. I need something compact like:

data Proof = Apply Proof Proof | S | K {- Haskell, combinatory logic -}

show/hide this revision's text 2 added 15 characters in body
show/hide this revision's text 1