Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Mechanizing Synthetic Tait Computability in Istari

Runming Li, Yue Yao, Robert Harper

TL;DR

This paper tackles the challenge of mechanizing Synthetic Tait Computability (STC) by embedding its gluing-based meta-theory inside Istari, an extensional Martin-Löf-style proof system with equality reflection. It develops a reusable library for synthetic phase distinctions (modalities, extension types, strict glue types) and applies STC to two nontrivial canonicity models, showing that core STC constructions translate essentially verbatim into machine-checked formalizations. The work demonstrates the practicality of mechanizing sophisticated meta-theoretic arguments in an extensional setting and argues that equality reflection helps maintain concise proofs with minimal transport overhead. Overall, it provides a proof-of-concept that STC can be effectively formalized in extensional proof assistants, offering a scalable path for future mechanizations of gluing-based meta-theory.

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.

Mechanizing Synthetic Tait Computability in Istari

TL;DR

This paper tackles the challenge of mechanizing Synthetic Tait Computability (STC) by embedding its gluing-based meta-theory inside Istari, an extensional Martin-Löf-style proof system with equality reflection. It develops a reusable library for synthetic phase distinctions (modalities, extension types, strict glue types) and applies STC to two nontrivial canonicity models, showing that core STC constructions translate essentially verbatim into machine-checked formalizations. The work demonstrates the practicality of mechanizing sophisticated meta-theoretic arguments in an extensional setting and argues that equality reflection helps maintain concise proofs with minimal transport overhead. Overall, it provides a proof-of-concept that STC can be effectively formalized in extensional proof assistants, offering a scalable path for future mechanizations of gluing-based meta-theory.

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.

Paper Structure

This paper contains 37 sections, 2 theorems, 16 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Gluing
  3. Synthetic Tait Computability
  4. Formalization of Synthetic Tait Computability
  5. Contributions
  6. A Refresher on STC
  7. Extension Types
  8. Strict Glue Types
  9. Syntax
  10. Canonicity Model
  11. Semantics of Judgments
  12. Semantics of Booleans
  13. Semantics of Dependent Products
  14. What Is So Synthetic About STC?
  15. The Proof Assistant
  16. ...and 22 more sections

Key Result

theorem 1

For every closed term of boolean type, represented as a morphism $b : \red{\terminal}_\T \to \red{\bool}_\T$ in $\T$, either $b = \red{\true}_\T$ or $b = \red{\false}_\T$.

Figures (2)

  • Figure 1: Inference rules for extension types
  • Figure 2: Inference rules for strict glue types

Theorems & Definitions (4)

  • theorem 1: Canonicity
  • definition 1
  • definition 2
  • theorem 2: Canonicity