Ende Jin, Nada Amin, and Yizhou Zhang. 6/2023. “Extensible Metatheory Mechanization via Family Polymorphism.” Proceedings of the ACM on Programming Languages, 7, PLDI. Publisher's Version