2020/11/08 by Pritam Choudhury, Choudhury, Pritam, Harley Eades III +5 · 3 citations
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.2011.04070
Extended version of paper with same title at POPL 2021, 39 pages
arxiv created 2021/01/06 · arxiv updated 2021/01/07
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.