Towards Graded Modal Dependent Types
summary
Graded Modal Dependent Type Theory (GrTT) defines dependent types indexed by a preordered semiring of grades to track resource use both at runtime and in types, recovering parametricity for exact-usage semirings and distinguishing specification-only assumptions. The implementation Gertie supports tensors, graded modalities, implicit grade inference and reports about a 30% speedup in type checking from erasing unused assumptions; first-class and user-defined semirings remain future work.
AI-written summary · about
chapters (6)
- 0:00Start
- 0:13Outline
- 0:45A brief history of grading linear and non-linear use (Girard, 1987)
- 4:56Typing judgments
- 6:01Example: polymorphic identity
- 8:39Revisiting the Motivation
related talks
19mCombining Dependency, Grades, and Adjoint Logic
27mPractical Extensions for Graded Monads
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
20mA Graded Modal Type Theory for Pulse Schedules
49mQuantitative program reasoning in Granule via graded modal types
29mTheoretical Foundations for Objects with Pattern Matching and GADT-Style Reasoning
18mGradual Typing for Effect Handlers
25mAdapTT: Functoriality for Dependent Type Casts