The Taming of the Rew: A Type Theory with Computational Assumptions

on YouTube ↗28m

" summary

Rewriting Type Theory lets users add user-defined rewrite rules as computational assumptions that the type checker applies automatically, not as noncomputational axioms. The paper formalizes RTT in MetaCoq, implements rewrite rules in Agda, and proves subject reduction provided a triangle (parallel reduction) confluence criterion holds; an automated checker verifies this modularly. Concrete wins: plus defined to compute on both arguments fixes commutativity proofs, and a quotient recursor gains computation so previously stuck goals are accepted.

AI-written summary · about

" chapters (14)

1. 0:00Start
2. 1:09The limitations of a proof assistant
3. 7:47Example #2: quotient types
4. 8:16Our contribution: Rewriting Type Theory
5. 9:42General shape of a rewrite rule
6. 12:42Metatheory of RTT
7. 13:10Logical consistency
8. 14:51Decidable typechecking
9. 18:47Re-establishing subject reduction through confluence
10. 20:04Some inspiration from the masters
11. 21:12The Tait-Martin-Löf criterion Triangle property: each t has optimal reduct p(t)
12. 23:02Checking the triangle property of rewrite rules in three steps
13. 25:54Conclusion
14. 27:07Want to learn more?