一句话：提出基于族多态的语言设计，使证明助手能复用和扩展元理论机械化代码与证明。
随着元理论机械化日益普及，证明助手亟需支持可复用、可扩展的代码与证明。本文提出一种面向证明助手可扩展元理论机械化的新语言设计，核心是借鉴面向对象的族多态，使代码与证明能相对其所在族进行多态化，从而在族扩展时自动复用和适配。该设计需应对证明助手底层语言兼具函数式、依赖类型、逻辑和交互式工具等特性带来的挑战。作者在 Coq 中实现插件原型，建立刻画该机制的依赖类型理论并证明其一致性与规范性，并通过案例研究展示新表达力能自然解决元理论机械化中的实际编程难题。
With the growing practice of mechanizing language metatheories, it has become ever more pressing that interactive theorem provers make it easy to write reusable, extensible code and proofs. This paper presents a novel language design geared towards extensible metatheory mechanization in a proof assistant. The new design achieves reuse and extensibility via a form of family polymorphism, an object-oriented idea, that allows code and proofs to be polymorphic to their enclosing families. Our development addresses technical challenges that arise from the underlying language of a proof assistant being simultaneously functional, dependently typed, a logic, and an interactive tool. Our results include (1) a prototypical implementation of the language design as a Coq plugin, (2) a dependent type theory capturing the essence of the language mechanism and its consistency and canonicity results, and (3) case studies showing how the new expressiveness naturally addresses real programming challenges in metatheory mechanization.
@article{paperbot1960,
title = {Extensible Metatheory Mechanization via Family Polymorphism},
author = {Ende Jin and Nada Amin and Yizhou Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591286}
}