Normal deduction in the intuitionistic linear logic

We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev. Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined with a construction \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $<\Gamma>$\end{document} introduced by the author to avoid cut-like constructions used in \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document} $\otimes$\end{document}-elimination and global restrictions employed by Prawitz. Normal form for natural deduction is obtained by Prawitz translation of cut-free sequent derivations.