A graded dependent type system with a usage-aware semantics (extended version)
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.
Keywords
Cite
@article{arxiv.2011.04070,
title = {A graded dependent type system with a usage-aware semantics (extended version)},
author = {Pritam Choudhury and Harley Eades and Richard A. Eisenberg and Stephanie C Weirich},
journal= {arXiv preprint arXiv:2011.04070},
year = {2021}
}
Comments
Extended version of paper with same title at POPL 2021, 39 pages