{"ID":2871450,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2509.11418","arxiv_id":"2509.11418","title":"Mechanizing Synthetic Tait Computability in Istari","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ö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.","short_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. Thi...","url_abs":"https://arxiv.org/abs/2509.11418","url_pdf":"https://arxiv.org/pdf/2509.11418v2","authors":"[\"Runming Li\",\"Yue Yao\",\"Robert Harper\"]","published":"2025-09-14T20:11:58Z","proceeding":"cs.PL","tasks":"[\"cs.PL\"]","methods":"[\"Generative Adversarial Network\"]","has_code":false}