Coco: Compositional Corecursion

Coco, which stands for compositional corecursion, is a Rocq library for compositional corecursive definition based on the CHP (Compositional Heterogeneous Productivity) theory.

For more information, please see:

• Jaewoo Kim, Yeonwoo Nam*, Chung-Kil Hur. Coco: Corecursion with Compositional Heterogeneous Productivity. POPL 2026.

(* The second author, Yeonwoo Nam, made significant contributions comparable to those of the first author.)

Installation

• Requirement : opam (>=2.1.0), Coq 8.20.0 (Currently, Rocq 9.0 is unavailable)

• Install dependencies with opam :

./configure

In the coco directory,

# from source
make

File Structure

The core of the CHP theory is implemented in the directories l1 (mainly first-order) and l2 (mainly second-order), building upon code from util, spfunctor, and l0.

Examples

See /src/example for examples.

• /src/example/README.md explains the contents of the examples.

Tutorials

See /src/tutorial for tutorials.

• /src/tutorial/README.md describes how to build the tutorials.
• /src/tutorial/t0_ToC.v explains the contents of the tutorials. Refer to the file for description of other tutorial files.

Tips

See /doc/tips.md for tips.

Used Axioms

Coco makes use of some well-established axioms for its implementation.

Core

• Function Extensionality (functional_extensionality_dep)
• Coinductive Extensionality (Bisimulation Equality for corecursive type) (see container_bisim_eq)
• Uniqueness of Identity Proof (UIP)
  • This axiom is known to be implied by excluded middle.
• Excluded Middle (classic)
• Choice (dependent_unique_choice)

Collateral

The axioms listed here are used only in specific parts of the code and, in principle, can be avoided in some cases.

• Strong Excluded Middle (excluded_middle_informative)
  • Only when (i) using fixpoints such as cfixpoint or (ii) using levels that rely on decidability such as level_if
  • You can avoid the case of (i) by using constructive fixpoints, such as fixpoint_constructive.
  • You can avoid the case of (ii) in instances where levels such as level_if are not used (e.g. nondegenerate function CTTs are not involved).
  • In the code, the alias strong_em is mainly used in place of excluded_middle_informative, to avoid dependency on the library file Coq.Logic.IndefiniteDescription.
• Constructive Definite Description (constructive_definite_description)
  • Only when using RSPFunctor
• Constructive Indefinite Description (constructive_indefinite_description)
  • Only when using cfixpoint_srwf