# Coco: Corecursion with Compositional Heterogeneous Productivity

Source: [Coco: Corecursion with Compositional Heterogeneous Productivity](<https://www.sota2.com/research/paper/6927dafdd6b0dd3342930ca1>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2025-11-28T05:02:18.972Z

Authors: Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur

Published: 2025-11-26T06:22:07.000Z

## Abstract

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.

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/2511.21093>)

[PDF](<https://arxiv.org/pdf/2511.21093.pdf>)