Label Dependent Lambda Calculus and Gradual Typing

on YouTube ↗15m

" summary

A small dependently typed core called the label-dependent lambda calculus models records as functions over first-class labels and adds lightweight Pi/Sigma/singleton types; a gradual extension adds the dynamic type and compiles into a cast calculus that forces type reduction to head normal form before runtime casts. The implementation includes a bidirectional type checker, algorithms for gradual consistent subtyping, decidable typechecking, and machine-checked proofs (Agda) of type soundness, progress, and the gradual guarantee*.

AI-written summary · about

" chapters (12)

1. 0:00Label Dependent Lambda Calculus and Gradual Typing
2. 0:27The Label Dependent Lambda Calculus (LDLC)
3. 1:16Example: Encoding Records
4. 4:05Example: Gradual Encoding of Records
5. 5:42Overall Approach
6. 7:14Outline
7. 7:33Bidirectional Typing for LDLC
8. 8:12Flexible Dependent Pairs
9. 9:25Narrowing Using Singleton Types
10. 11:19Type Reduction at Run Time (Cast Calculus)
11. 12:54Metatheory
12. 13:21Contributions