Separating weakening and contraction in a linear lambda calculus

We present a separated-linear lambda calculus based on a
refinement of linear logic which allows separate control of
weakening and contraction. The calculus satisfies subject reduction
and confluence, has a straightforward notion of standard evaluation,
and inherits previous results on the relationship of Girard's two
translations from minimal intuitionistic logic to linear logic with
call-by-name and call-by-value. We construct a hybrid translation from
Girard's two which is sound and complete for mapping types, reduction
sequences and standard evaluation sequences from call-by-need into
separated-linear lambda, a more satisfying treatment of call-by-need
than in previous work, which now allows a contrasting of all three
reduction strategies in the manner (for example) that the CPS transla-
tions allow for call-by-name and call-by-value.