Toward lambda-calculi for linear logic