Normalization by Evaluation for Non-cumulativity

on YouTube ↗21m

" summary

Claims that untyped NbE for non-cumulativity is sound and complete for a Martin-Löf style type theory with explicit universe levels, gives a mechanized proof in a proof assistant, and produces a working NbE algorithm that still works after erasing those explicit annotations. Proof strategy builds an annotated syntax, a level-aware syntactic semantic domain, a PER model for η and β, and a gluing model for soundness. Artifacts and mechanization are available and reusable mechanized proof.

AI-written summary · about

" chapters (18)

1. 0:00Normalization by evaluation intro
2. 0:23Dependent types background
3. 1:46Cumulativity vs non-cumulativity
4. 3:53Universe level annotations
5. 5:18MBE technique overview
6. 6:20MBE non-cumulative challenges
7. 7:24Non-cumulative solution
8. 8:30Syntax and typing rules
9. 9:52Semantic domain for MBE
10. 10:56Evaluation and reification
11. 11:18Meta-theory with subs
12. 12:21PER model
13. 13:04Glueing model
14. 13:45MBE soundness consequences
15. 14:27Removing annotations
16. 15:29Annotated vs unannotated
17. 16:55Conclusion and proofs
18. 18:38Q&A