Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally

on YouTube ↗27m

" summary

Claims a type theory LRTT that adds local rewrite rules via prenex abstraction over computation rules and a prototype implemented as a Rocq extension with all results formalised in Rocq. It shows a conservative embedding into Martin‑Löf type theory by a definition inlining (monomorphisation) procedure, encapsulates dangerous global rewrites, hides implementations (W‑types, quotients), and works in the prototype while relying on rewrite termination and confluence checks (prototype uses a triangle criterion). Artifacts and a planned Rocq 9.3 integration are provided.

AI-written summary · about

" chapters (14)

1. 0:00Local computation control
2. 1:26Definitional equality limits
3. 3:53Rewrite rules for control
4. 6:45Dangers of global rewrites
5. 7:26Local rewriting theory
6. 9:11Hiding with LRT
7. 10:36Strictifications and encodings
8. 12:04LRT typing rules
9. 14:34LRT properties and conservativity
10. 17:05Rewrite rules challenges
11. 18:10Rocq implementation
12. 18:51Quotient types with LRT
13. 19:55Conclusion and future
14. 21:04Q&A