Coco: Corecursion with Compositional Heterogeneous Productivity
summary
CHP claims it computes Compositional Heterogeneous Productivity relations that quantify how many outputs a component produces given input-level requirements, letting productivity compose by relation composition and disjunction. Coco for Rocq implements this and automates productivity inference, second-order reasoning, and fixed-point generation using combinator translations and an NIA-based tactic; it accepts examples rejected by Coq-style guardedness (zeros, growing, S2) and finds S1 ill defined. Artifacts and proof scripts are available (DOI 10.5281/zenodo.17347133).
AI-written summary · about
chapters (10)
- 0:00Coco framework intro
- 0:51Coinductive types basics
- 2:15Well-defined vs ill-defined corecursion
- 4:45Limitations of existing solutions
- 6:57Compositional Heterogeneous Productivity
- 12:45CHP theory with level sets
- 17:01Productivity lemmas in Coco
- 19:30Automating productivity checks
- 21:58Conclusion and future
- 23:03Q&A
related talks
19mCertified Compilers à la Carte
21mCompositional pre-processing for automated reasoning in dependent type theory
58mCoalgebra for the working programming languages researcher
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
31mA Coq Library of Undecidable Problems
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders