A Graded Dependent Type System with a Usage-Aware Semantics

Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop a novel version of such a graded dependent type system, including 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 usage of resources. Several useful properties, including the standard type soundness theorem, non-interference of irrelevant resources and single pointer property for linear resources, can be derived from this theorem. We expect that our work will provide a base for integrating linearity, irrelevance and dependent types in practical programming languages like Haskell.