一句话：提出 CHP 框架与 Rocq 库 Coco，通过组合式异构生产性自动化支持广泛余递归定义。
证明助手通常依赖严格的语法守卫条件来保证余递归定义的生产性，这拒绝了许多合法定义；已有方法在覆盖范围与自动化之间难以兼顾。本文提出组合式异构生产性（CHP）理论框架，将生产性推广到定义域和余定义域类型各异的函数，包括非余归纳类型，并强调组合性：复合函数的生产性可由其组成部分系统计算，从而支持复杂余递归模式的模块化推理。基于 CHP，作者实现 Rocq 库 Coco，为生产性计算与不动点生成提供广泛自动化。该工作统一了高自动化与广覆盖，扩展了证明助手中余递归定义的可用性。
Contemporary proof assistants impose restrictive syntactic guardedness conditions that reject many valid corecursive definitions. Existing approaches to overcome these restrictions present a fundamental trade-off between coverage and automation. We present Compositional Heterogeneous Productivity (CHP), a theoretical framework that unifies high automation with extensive coverage for corecursive definitions. CHP introduces heterogeneous productivity applicable to functions with diverse domain and codomain types, including non-coinductive types. Its key innovation is compositionality: the productivity of composite functions is systematically computed from their components, enabling modular reasoning about complex corecursive patterns. Building on CHP, we develop Coco, a corecursion library for Rocq that provides extensive automation for productivity computation and fixed-point generation.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-21093,
title = {Coco: Corecursion with Compositional Heterogeneous Productivity},
author = {Jaewoo Kim and Yeonwoo Nam and Chung-Kil Hur},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776733}
}