{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:14:09Z","timestamp":1784211249292,"version":"3.55.0"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>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.<\/jats:p>\n                  <jats:p>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.<\/jats:p>\n                  <jats:p>Building on CHP, we develop Coco, a corecursion library for Rocq that provides extensive automation for productivity computation and fixed-point generation.<\/jats:p>","DOI":"10.1145\/3776733","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2643-2671","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Coco: Corecursion with Compositional Heterogeneous Productivity"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-8789-5996","authenticated-orcid":false,"given":"Jaewoo","family":"Kim","sequence":"first","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0837-4573","authenticated-orcid":false,"given":"Yeonwoo","family":"Nam","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1656-0913","authenticated-orcid":false,"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Andreas Abel and James Chapman. 2014. Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types. arXivpreprint arXiv:1406.2059 (2014). https:\/\/doi.org\/10.48550\/arXiv.1406.2059 10.48550\/arXiv.1406.2059","DOI":"10.48550\/arXiv.1406.2059"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.6"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_5"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_15"},{"key":"e_1_3_2_7_2","unstructured":"Minki Cho. [n.d.]. semantic-strict-positivity. https:\/\/github.com\/minkiminki\/semantic-strict-positivity Accessed: [2025-10-21]."},{"key":"e_1_3_2_8_2","unstructured":"The Lean Development. [n.d.]. The Lean Theorem Prover. https:\/\/lean-lang.org Accessed: [2025-07-10]."},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209148"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_3_2_13_2","unstructured":"INRIA. [n.d.]. The Rocq Prover. http:\/\/coq.inria.fr Accessed: [2025-07-10]."},{"key":"e_1_3_2_14_2","unstructured":"INRIA. [n.d.]. The Rocq Prover Document. https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/index.html Accessed: [2025-07-10]."},{"key":"e_1_3_2_15_2","volume-title":"Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips","author":"Jones Geraint","year":"1993","unstructured":"Geraint Jones and Jeremy Gibbons. 1993. Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips. Technical Report No. 71. Dept of Computer Science, University of Auckland. http:\/\/www.cs.ox.ac.uk\/people\/jeremy.gibbons\/publications\/linear.ps.gz Also IFIP Working Group 2.1 working paper 705 WIN-2."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Jaewoo Kim Yeonwoo Nam and Chung-Kil Hur. 2025. Artifact for \"Coco: Corecursion with Compositional Heterogeneous Productivity\" POPL 2026. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.17347133 10.5281\/zenodo.17347133","DOI":"10.5281\/zenodo.17347133"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Jaewoo Kim Yeonwoo Nam and Chung-Kil Hur. 2025. Coco: Corecursion with Compositional Heterogeneous Productivity. https:\/\/doi.org\/10.48550\/arXiv.2511.21093 10.48550\/arXiv.2511.21093 arXiv:2511.21093 [cs.LO]","DOI":"10.48550\/arXiv.2511.21093"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009880"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-5(3:10)2009"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_6"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00012-9"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/5.2.231"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Tobias Nipkow Markus Wenzel and Lawrence C. Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Springer-Verlag Berlin Heidelberg. https:\/\/doi.org\/10.1007\/3-540-45949-9 10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934564"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Vlad Rusu and David Nowak. 2022. Defining Corecursive Functions in Coq Using Approximations. In 36th European Conference on Object-Oriented Programming (ECOOP 2022) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 222) Karim Ali and Jan Vitek (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 12:1-12:24. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.12 10.4230\/LIPIcs.ECOOP.2022.12","DOI":"10.4230\/LIPIcs.ECOOP.2022.12"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00063-5"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002527"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57418-9_17"},{"key":"e_1_3_2_32_2","unstructured":"Youngju Song Minki Cho Dongjae Lee Chung-Kil Hur Michael Sammler and Derek Dreyer. 2023. Conditional Contextual Refinement. Proc. ACM Program. Lang. 7 POPL Article 39 (Jan. 2023) 31 pages. https:\/\/doi.org\/10.11453571232 10.11453571232"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.75"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Li-yao Xia Yannick Zakowski Paul He Chung-Kil Hur Gregory Malecha Benjamin C. Pierce and Steve Zdancewic. 2019. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang. 4 POPL Article 51 (Dec. 2019) 32 pages. https:\/\/doi.org\/10.1145\/3371119 10.1145\/3371119","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776733","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:39:25Z","timestamp":1784209165000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776733"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":33,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776733"],"URL":"https:\/\/doi.org\/10.1145\/3776733","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}