[CPP'26] Mechanizing Synthetic Tait Computability in Istari

Mechanizing Synthetic Tait Computability in Istari (Video, CPP 2026) Runming Li, Yue Yao, Robert Harper (Carnegie Mellon University, USA; Carnegie Mellon University, USA; Carnegie Mellon University, USA) Abstract: Categorical gluing is a powerful technique for proving meta-theorems of type theories such as canonicity and normalization. Synthetic Tait Computability (STC) provides an abstract treatment of the complex gluing models by internalizing the gluing category into a modal dependent type theory with a phase distinction. This work presents a mechanization of STC in the Istari proof assistant. Istari is a Martin-L\"{o}f-style extensional type theory with equality reflection, which avoids much of the explicit transport reasoning typically found in intensional proof assistants. This work develops a reusable library for synthetic phase distinction, including modalities, extension types, and strict glue types, and applies it to two case studies: (1) a canonicity model for dependent type theory with dependent products and booleans with large elimination, and (2) a Kripke canonicity model for the cost-aware logical framework. Our results demonstrate that the core STC constructions can be formalized essentially verbatim in Istari, preserving the elegance of the on-paper arguments while ensuring machine-checked correctness. Article: https://doi.org/10.1145/3779031.3779085 Supplementary archive: https://doi.org/10.5281/zenodo.17808361 (Badges: Artifacts Available) ORCID: https://orcid.org/0000-0001-7600-9069, https://orcid.org/0000-0001-8523-5156, https://orcid.org/0000-0002-9400-2941 Video Tags: gluing, synthetic Tait computability, logical relations, extensional type theory, Istari, equality reflection, meta-theory, cost-aware logical framework, doi:10.1145/3779031.3779085, doi:10.5281/zenodo.17808361, orcid:0000-0001-7600-9069, orcid:0000-0001-8523-5156, orcid:0000-0002-9400-2941, Artifacts Available Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ Sponsored by ACM SIGPLAN.