Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
summary
Presents a denotational model of a simple gradually typed lambda calculus built inside guarded type theory, solving the dynamic-type equation with guarded recursion and proving beta‑eta equality plus the graduality theorem. Reconciles step sensitivity with transitivity via a lock-step ordering plus explicit syntactic perturbations and proves a no‑go result for unrestricted step‑insensitivity. Most core theorems are mechanized in Guarded Cubical Agda; the model yields a partial semantics (nat | error) and scales toward adding higher‑order store and alternative cast strategies.
AI-written summary · about
chapters (18)
- 0:00Gradual typing semantics intro
- 1:05Key properties of gradual typing
- 2:31Modeling gradual typing challenges
- 3:53Classical domain theory limits
- 4:55Guarded type theory solution
- 6:21Guarded type theory intent
- 6:42Denotational semantics for gradual typing
- 7:45Modeling effectful programs
- 8:52Dynamic typing with guarded recursion
- 10:15Type and term precision
- 11:38Casts and graduality axioms
- 12:21Modeling precision approach
- 13:25Precision step insensitivity conflict
- 14:47Synchronizing terms with perturbations
- 15:49Final model structure
- 16:54Formalization in guarded cubical Agda
- 17:15Summary and future work
- 17:38Q&A