Label dependent lambda calculus and gradual typing

on YouTube ↗29m

" summary

Defines a minimalist label-dependent lambda calculus with first-class labels, Pi/Sigma/singleton types and subtyping, then gives a gradual extension with a bidirectional type checker that translates surface programs into an explicit cast calculus. Key innovations: refined cast typing for singletons, type reduction inside casts, and fully dependent Sigma handling; proofs include type safety, decidability of type checking, and the gradual guarantee. An implementation and partial mechanization exist and the cast-driven runtime enforces checks to prevent mistyped executions.

AI-written summary · about

" chapters (11)

1. 0:00Label dependent lambda calculus
2. 1:07Label dependent types
3. 3:17Records with label dependencies
4. 5:40Gradual typing in dependent systems
5. 10:14Gradual language design
6. 13:56Bidirectional typing
7. 17:26Dependent pairs in call-by-value
8. 20:58Casts and type reduction
9. 23:02Meta-theory and guarantees
10. 24:05Implementation and future work
11. 28:08Q&A