In this paper, we present a novel calculus of inductive linear constructions (CILC), combining linear types and dependent types. Our type theory addresses a looming issue in the research on linear dependent types: the lack of a general mechanism for defining sound linear inductive types. CILC allows one to encode in a straightforward manner the linear connectives that must be baked into the core of other systems. This greatly lowers the difficulty of encoding various data structures and makes writing non-trivial programs humanly feasible. We study the standard meta theory of our calculus, showing that it is sound in the usual sense. Through a heap-based operational semantics, we show that CILC safely manipulates resources and runs memory clean. We have formalized and proven correct most of the reported results in the Coq Proof Assistant.