nLab linear lambda-calculus

Idea

Under the Curry-Howard correspondence, proofs of intuitionistic logic can be seen at $\lambda$-terms. In the same way, one can see proofs of linear logic as terms of a linear $\lambda$-calculus. It allows one to have a more compact syntax for proofs of linear logic which can be more practical to analyze their computational properties. Under this correspondence, the cut-elimination of proofs corresponds to the $\beta$-reduction of terms.