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{*}$, 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 wildly impractical in terms of performance.

翻译：Coq 等当代证据助理要求循环功能终止,核心精度功能要富有成效,以保持其类型理论的逻辑一致性,有些则通过合成检查确保这些属性。然而,由于这些功能具有内在的微妙性和限制性,因此用户无法轻易地写成明显终止或生产功能,因此无法随心所欲地完成。与此同时,有许多规模大的理论,可以进行基于类型终止和生产力检查,包括基于(Co)诱导建设(Co)的计算法(CIC)的计算法(CIC)的理论,核心计算法(CIC)的核心计算法。这些理论比较起来更加可靠,而且具有构成性。这些理论为什么没有适应Coq?在本论文中,我们冒昧地用CIC$/blushat_$这个以CIC为基础的规模型理论来回答这一问题。它扩展了CIC公司以往关于规模的分类方法,增加了全球和地方定义等特点。我们还在Coq 骨架内提出了相应的推算法(Coq ) 。这些理论与现有的野行发展相匹配,因此不需要再用不切实际的图表来解释。