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.

Created on February 19, 2023 at 06:35:37. See the history of this page for a list of all contributions to it.