Gradual Metaprogramming

on YouTube ↗31m

" summary

A calculus called MetaGTLC models a gradually typed metalanguage that generates statically typed object code and compiles to an explicit cast calculus MetaCC; the implementation adds a quote coercion to force (and blame) type checks during metaevaluation rather than at runtime, uses a coercion combinator reduction for explicit casts, and requires birectional checking to synthesize target types at splices. The result is a mechanized type-safety proof and executable artifacts checked in Agda, ensuring generated object programs are well typed or blame early.

AI-written summary · about

" chapters (14)

1. 0:00Introduction
2. 1:03Gradual typing meets metaprogramming
3. 3:55Meta language syntax and types
4. 6:06Compiling to cast calculus
5. 7:30Quoted coercions and reduction
6. 11:43Design differences from prior work
7. 16:22Type-directed compilation rules
8. 17:26Why bidirectional typing
9. 21:25Type safety and formalization
10. 22:28Conclusion
11. 23:34Q&A: Bidirectional typing limits
12. 24:18Q&A: Coercion tradeoffs
13. 26:06Q&A: Type info and errors
14. 29:28Q&A: Static typing in splices