A graded dependent type system with a usage-aware semantics

Pritam Choudhury, Harley Eades, Richard A. Eisenberg, Stephanie Weirich

Research output: Contribution to journalArticlepeer-review

10 Scopus citations


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.

Original languageEnglish (US)
Article number50
JournalProceedings of the ACM on Programming Languages
Issue numberPOPL
StatePublished - Jan 2021


  • Irrelevance
  • heap semantics
  • linearity
  • quantitative reasoning

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'A graded dependent type system with a usage-aware semantics'. Together they form a unique fingerprint.

Cite this