Robust Dynamic Embedding for Gradual Typing
summary
Defines Robust Dynamic Embedding as a new adequacy criterion: if a dynamic component semantically satisfies a static type then its embedding ascribed to that type never fails because of its own casts. Proves RDE is independent of existing criteria, exhibits counterexamples where common gradual semantics fail, and implements a gradualized simply‑typed language that satisfies RDE using lazy downcasts and logical relations. All results are mechanized in the Rocq proof assistant (artifacts available).
AI-written summary · about
chapters (8)
- 0:00Introduction
- 3:34Gradual typing and runtime checks
- 8:52Robust dynamic embedding criterion
- 11:41Criterion trivial or attainable
- 16:46Criterion realism and counterexamples
- 18:13Formal proof and semantic typing
- 21:49Conclusion and future work
- 22:13Q&A
related talks
19mA Dependently Typed Language with Dynamic Equality
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
28mGoing Static, Gradually: Semantic Soundness and Telling the Truth at Scale
19mContextual Embeddings: Implementing Bound Variables through Instance Resolution
15mA compilation method for dynamic typing in ML
19mCombining Dependency, Grades, and Adjoint Logic
27mLightweight Semantics Engineering with Redex
21mGradual Typing is the best!