Linear Lambda Calculus and Deep Inference

We introduce a deep inference logical system SBVr which extends SBV with Rename, a self-dual atom-renaming operator. We prove that the cut free subsystem BVr of SBVr exists. We embed the terms of linear lambda-calculus with explicit substitutions into formulas of SBVr. Our embedding recalls the one of full lambda-calculus into pi-calculus. The proof-search inside SBVr and BVr is complete with respect to the evaluation of linear lambda-calculus with explicit substitutions. Instead, only soundness of proof search in SBVr holds. Rename is crucial to let proof-search simulate the substitution of a linear lambda-term for a variable in the course of linear beta-reduction. Despite SBVr is a minimal extension of SBV its proof-search can compute all boolean functions, exactly like linear lambda-calculus with explicit substitutions can do.