一句话：提出 CIC* sized type theory 与 size inference 并实现于 Coq 内核，评估发现性能严重退化，结论不实用。
证明助手 Coq 要求递归函数终止、余递归函数生产，以维持类型论一致性，但其句法检查脆弱且限制用户；已有 sized type theories 更稳健、可组合，却未用于 Coq。为回答原因，本文提出 CIC*：基于 CIC 的 sized type theory，扩展了全局与局部定义等 Coq 特性。作者设计相应 size inference 算法并在 Coq 内核中实现；为最大向后兼容，无需用户额外标注。评估编译 Coq 标准库部分内容时，发现算法本身导致严重性能退化。结论：若要保持向后兼容，用 size inference 替代句法检查在性能上不切实际。
Abstract Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim. Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven’t they been adapted to Coq? In this paper, we venture to answer this question with CIC $\widehat{\ast}$ , a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq’s kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user. In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is impractical in terms of performance.