A Unified View of Modalities in Type Systems
summary
Proposes a single algebraic structure of modalities embedded in System F that recovers linear, usage-counting, security, sensitivity and belief-style systems and proves key meta results: substitution lemma, modality-annotated context rules, an operational modality-preserving abstract machine and Kripke-style semantics using division/Galois connections. Shows addition distributes over meet, gives an irrelevance theorem (zero-annotated variables are never used), and reports that the framework captures many prior modal type systems and their metatheory, so the design is implemented and the proofs go through.
AI-written summary · about
chapters (14)
- 0:00Start
- 0:32Motivation
- 1:24Framework: Polymorphic Lambda Calculus (subset)
- 1:34Curry-Howard isomorphism
- 1:58Key idea (1)
- 4:59Modality structure: summary
- 5:24Application: Linear types
- 5:44"Quantitative" System F
- 6:18Lattice The lattice can be used for many purposes.
- 7:39Sensitivity analysis for differential privacy
- 7:50Substitution Lemma
- 8:24Abstract machine
- 8:47Relational semantics
- 11:15Conclusion and Future work
related talks
14mModal Effect Types
20mModal Mu-Calculus for Free in Agda
18mA modal deconstruction of Löb induction
16mS4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
18mThe Essence of Generalized Algebraic Data Types
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
19mCombining Dependency, Grades, and Adjoint Logic
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction