  Graded Type Theory provides a mechanism to track and reason about resource
usage in type systems. In this paper, we develop GraD, a novel version of such
a graded dependent type system that includes functions, tensor products,
additive sums, and a unit type. Since standard operational semantics is
resource-agnostic, we develop a heap-based operational semantics and prove a
soundness theorem that shows correct accounting of resource usage. Several
useful properties, including the standard type soundness theorem,
non-interference of irrelevant resources in computation and single pointer
property for linear resources, can be derived from this theorem. We hope that
our work will provide a base for integrating linearity, irrelevance and
dependent types in practical programming languages like Haskell.
