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

Abstract

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
Volume5
Issue numberPOPL
DOIs
StatePublished - Jan 2021

Keywords

  • Irrelevance
  • heap semantics
  • linearity
  • quantitative reasoning

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

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

Cite this