Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 22-minute conference presentation from CPP 2026 that demonstrates the mechanization of Synthetic Tait Computability (STC) in the Istari proof assistant. Learn how researchers from Carnegie Mellon University formalized categorical gluing techniques for proving meta-theorems of type theories such as canonicity and normalization. Discover how STC provides an abstract treatment of complex gluing models by internalizing the gluing category into a modal dependent type theory with phase distinction. Examine the advantages of using Istari, a Martin-Löf-style extensional type theory with equality reflection that avoids explicit transport reasoning typically required in intensional proof assistants. Study the development of a reusable library for synthetic phase distinction, including modalities, extension types, and strict glue types. Analyze two practical case studies: a canonicity model for dependent type theory with dependent products and booleans with large elimination, and a Kripke canonicity model for the cost-aware logical framework. Understand how the core STC constructions can be formalized essentially verbatim in Istari while preserving the elegance of theoretical arguments and ensuring machine-checked correctness. Access supplementary materials including the full research paper and artifact archive for hands-on exploration of the mechanized proofs and library implementations.
