Runming Li, Yue Yao, Robert Harper: Mechanizing Synthetic Tait Computability in Istari. CPP 2026: 231-247