Gradually Typed Languages Should Be Vigilant!
summary
Defines vigilance as a semantic criterion that checks whether runtime enforcement preserves the full run-time typing history; implements it by instrumenting operational semantics with a value log and extending a logical-relation proof with store/type-history bookkeeping. Proves Natural gradual typing is vigilant for the simple type system, Transient is not (but is vigilant for tag typing), and builds a new truer static system—stronger than tag typing—that matches Transient’s actual guarantees and enables simple check-removal optimizations.
AI-written summary · about
chapters (14)
- 0:00Vigilant gradual typing intro
- 1:27Untyped library interface problems
- 3:12Type soundness spectrum
- 5:18Complete monitoring limits
- 6:42Introducing vigilance property
- 9:12Formalizing vigilance logically
- 10:38Proving vigilance recipe
- 11:20Vigilance spectrum distinctions
- 12:46Designing truer transient types
- 15:14Flow sensitivity optimizations
- 16:20Future work conjectures
- 17:02Summary and conclusion
- 17:24Q&A: Closures and mutables
- 18:25Q&A: Error messages and blame
related talks
47mInformation Flow Types, Runtime Monitors, and Gradual Typing
23mGradual Verification for Smart Contracts
28mType-directed Program Transformation for Constant-Time Enforcement
22mQuest Complete: The Holy Grail of Gradual Security
26mType-directed Program Transformation for Constant-Time Enforcement
18mScalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)
22mReconciling Progress-Intensive Noninterference and Declassification
20mThe Downgrading Semantics of Memory Safety