.png){kind=icon}
.png){kind=icon}
Return
Coco: Corecursion with Compositional Heterogeneous Productivity
.png){kind=icon}
PRE
AI
DOI：10.1145/3776733.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
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.
Keywords:
Rocq
coinduction
corecursion
compositionality
interactive theorem proving
semantic productivity
Journal
P
IF:
2.8
Papers:
308
Citations:
4.7K