A Graded Dependent Type System with a Usage-Aware Semantics

on YouTube ↗31m

" summary

Presents Grad, a dependent type calculus with natural-number grades and separate demand contexts for terms and types, plus a heap-based reduction using graded heaps that enforces substituting exactly q occurrences. Proves a usage-aware soundness theorem: if a heap meets a context then evaluation never gets stuck, letting the authors derive standard type soundness, safe erasure of 0-graded arguments, non-interference of irrelevant resources and a single-pointer property for linear resources; mechanization and the POPL 2021 paper provide full proofs and examples.

AI-written summary · about

" chapters (22)

1. 0:00Intro
2. 0:49Making Sandwich
3. 1:46Grades: Precise Description of Demands
4. 2:50Graded Type Theory: A Brief Introduction
5. 5:06Why Graded Dependent Type Theory? Linearity and Dependent Types
6. 6:29Why Graded Dependent Type Theory? Erasure
7. 7:29Why Graded Dependent Type Theory? Some "Free Theorems"
8. 8:49A Graded Simple Calculus: What do we need?
9. 9:53A Graded Simple Calculus: Type System
10. 11:57Graded Type System: From Simple to Dependent
11. 14:58Principles of Counting Demand: A Comparison
12. 17:29GRAD: A Graded Dependent Type System
13. 18:21GRAD: Type Soundness
14. 19:13GRAD: Soundness of Demand Tracking?
15. 20:26GRAD: A Graded Heap Semantics
16. 21:51GRAD: Heap Reduction Relation
17. 23:49GRAD: Formal Soundness Theorem
18. 25:24GRAD: Soundness Example
19. 26:42GRAD: A Free Theorem
20. 28:54GRAD: Soundness Applications
21. 29:40Summary: What and How is GRAD?
22. 30:18Summary: Why GRAD?