Coco: Corecursion with Compositional Heterogeneous Productivity
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914171431419904 |
|---|---|
| author | Kim, Jaewoo Nam, Yeonwoo Hur, Chung-Kil |
| author_facet | Kim, Jaewoo Nam, Yeonwoo Hur, Chung-Kil |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_21093 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Coco: Corecursion with Compositional Heterogeneous Productivity Kim, Jaewoo Nam, Yeonwoo Hur, Chung-Kil Logic in Computer Science 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. |
| title | Coco: Corecursion with Compositional Heterogeneous Productivity |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2511.21093 |