Mechanizing Synthetic Tait Computability in Istari

on YouTube ↗22m

" summary

Mechanization of Synthetic Tait Computability is formalized in the Istari extensional type theory with equality reflection, producing a reusable library of modalities, extension types, strict glue types and two complete case studies: a canonicity model for dependent type theory with pi and booleans (large elimination) and a Kripke canonicity model for the cost‑aware logical framework. Core STC constructions translate virtually verbatim, avoiding transport hell; typical tactic proofs run ~100 lines for booleans, ~200–300 for pis and ~1000 for large elimination, and all results are machine‑checked with artifacts available.

AI-written summary · about

" chapters (15)

1. 0:00Synthetic Tait computability intro
2. 1:03Canonicity theorem example
3. 3:30Categorical proof interpretation
4. 5:16Synthetic Tait computability explained
5. 7:02Synthetic approach details
6. 9:36Transport reasoning in proofs
7. 10:59Extism proof assistant intro
8. 13:07Type checking in Extism
9. 14:11Phase distinction mechanized
10. 15:37Canonicity models overview
11. 16:42Comparison with intentional provers
12. 18:11Conclusion and future work
13. 19:19Q&A: Reproducing in other provers
14. 20:50Q&A: Nuprl historical comparison
15. 21:32Q&A: Extism user experience