{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:13Z","timestamp":1750220053073,"version":"3.41.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>\n            This paper proposes a new approach to writing and verifying divide-and-conquer programs in Coq. Extending the rich line of previous work on algebraic approaches to recursion schemes, we present an algebraic approach to divide-and-conquer recursion: recursions are represented as a form of algebra, and from outer recursions, one may initiate inner recursions that can construct data upon which the outer recursions may legally recurse. Termination is enforced entirely by the typing discipline of our recursion schemes. Despite this, our approach requires little from the underlying type system, and can be implemented in System\n            <jats:italic>F<\/jats:italic>\n            <jats:sub>\u03c9<\/jats:sub>\n            plus a limited form of positive-recursive types. Our implementation of the method in Coq does not rely on structural recursion or on dependent types. The method is demonstrated on several examples, including mergesort, quicksort, Harper\u2019s regular-expression matcher, and others. An indexed version is also derived, implementing a form of divide-and-conquer induction that can be used to reason about functions defined via our method.\n          <\/jats:p>","DOI":"10.1145\/3571196","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"61-90","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Type-Based Approach to Divide-and-Conquer Recursion in Coq"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7790-6116","authenticated-orcid":false,"given":"Pedro","family":"Abreu","sequence":"first","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1016-6261","authenticated-orcid":false,"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6237-3326","authenticated-orcid":false,"given":"Alex","family":"Hubers","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5434-5018","authenticated-orcid":false,"given":"Christa","family":"Jenkins","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3992-1080","authenticated-orcid":false,"given":"J. Garrett","family":"Morris","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9720-0003","authenticated-orcid":false,"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[{"name":"University of Iowa, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7305612"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2020.2"},{"key":"e_1_2_1_3_1","first-page":"234","volume-title":"Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (Tokyo, Japan) ( ICFP '11). ACM","author":"Ahn Ki Yung","year":"2011","unstructured":"Ki Yung Ahn and Tim Sheard . 2011 . A Hierarchy of Mendler Style Recursion Combinators: Taming Inductive Datatypes with Negative Occurrences . In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (Tokyo, Japan) ( ICFP '11). ACM , New York, NY, USA , 234 - 246 . Ki Yung Ahn and Tim Sheard. 2011. A Hierarchy of Mendler Style Recursion Combinators: Taming Inductive Datatypes with Negative Occurrences. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (Tokyo, Japan) ( ICFP '11). ACM, New York, NY, USA, 234-246."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.46"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129503004122"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01049178"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.042"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_1"},{"key":"e_1_2_1_11_1","volume-title":"Bird and Oege de Moor","author":"Richard","year":"1997","unstructured":"Richard S. Bird and Oege de Moor . 1997 . Algebra of programming. Prentice Hall . Richard S. Bird and Oege de Moor. 1997. Algebra of programming. Prentice Hall."},{"key":"e_1_2_1_12_1","first-page":"1","article-title":"Inductive types in the Calculus of Algebraic Constructions","volume":"65","author":"Blanqui Fr\u00e9d\u00e9ric","year":"2005","unstructured":"Fr\u00e9d\u00e9ric Blanqui . 2005 . Inductive types in the Calculus of Algebraic Constructions . Fundam. Informaticae 65 , 1 - 2 ( 2005 ), 61-86. http:\/\/content.iospress.com\/articles\/fundamenta-informaticae \/fi65-1-2-04 Fr\u00e9d\u00e9ric Blanqui. 2005. Inductive types in the Calculus of Algebraic Constructions. Fundam. Informaticae 65, 1-2 ( 2005 ), 61-86. http:\/\/content.iospress.com\/articles\/fundamenta-informaticae \/fi65-1-2-04","journal-title":"Fundam. Informaticae"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000115"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000283"},{"key":"e_1_2_1_16_1","volume-title":"Bowman","author":"Chan Jonathan","year":"2019","unstructured":"Jonathan Chan and William J . Bowman . 2019 . Practical Sized Typing for Coq. CoRR abs\/ 1912.05601 ( 2019 ). arXiv: 1912.05601 http:\/\/arxiv.org\/abs\/ 1912.05601 Jonathan Chan and William J. Bowman. 2019. Practical Sized Typing for Coq. CoRR abs\/ 1912.05601 ( 2019 ). arXiv: 1912.05601 http:\/\/arxiv.org\/abs\/ 1912.05601"},{"volume-title":"The Optimal Fixed Point Combinator","author":"Chargu\u00e9raud Arthur","key":"e_1_2_1_17_1","unstructured":"Arthur Chargu\u00e9raud . 2010. The Optimal Fixed Point Combinator . In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 195-210. Arthur Chargu\u00e9raud. 2010. The Optimal Fixed Point Combinator. In Interactive Theorem Proving, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 195-210."},{"key":"e_1_2_1_18_1","unstructured":"Arthur Chargu\u00e9raud. 2021. The TLC Coq Library. https:\/\/github.com\/charguer\/tlc  \t\t\t\t  Arthur Chargu\u00e9raud. 2021. The TLC Coq Library. https:\/\/github.com\/charguer\/tlc"},{"key":"e_1_2_1_19_1","unstructured":"Guillaume Claret. 2021. Coq of Ocaml. https:\/\/github.com\/clarus\/coq-of-ocaml. Accessed: 2021-09-09.  \t\t\t\t  Guillaume Claret. 2021. Coq of Ocaml. https:\/\/github.com\/clarus\/coq-of-ocaml. Accessed: 2021-09-09."},{"key":"e_1_2_1_20_1","volume-title":"Strong Categorical Datatypes I. In International Meeting on Category Theory 1991 (Canadian Mathematical Society Proceedings), R. A. G. Seely (Ed.). AMS.","author":"Cockett Robin","year":"1992","unstructured":"Robin Cockett and Dwight Spencer . 1992 . Strong Categorical Datatypes I. In International Meeting on Category Theory 1991 (Canadian Mathematical Society Proceedings), R. A. G. Seely (Ed.). AMS. Robin Cockett and Dwight Spencer. 1992. Strong Categorical Datatypes I. In International Meeting on Category Theory 1991 (Canadian Mathematical Society Proceedings), R. A. G. Seely (Ed.). AMS."},{"key":"e_1_2_1_21_1","volume-title":"Programming Languages-18th Brazilian Symposium, SBLP","author":"Copello Ernesto","year":"2014","unstructured":"Ernesto Copello , Alvaro Tasistro , and Bruno Bianchi . 2014. Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda . In Programming Languages-18th Brazilian Symposium, SBLP 2014 , Maceio, Brazil, October 2-3, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8771 ), Fernando Magno Quint\u00e3o Pereira (Ed.). Springer , 62-76. Ernesto Copello, Alvaro Tasistro, and Bruno Bianchi. 2014. Case of (Quite) Painless Dependently Typed Programming: Fully Certified Merge Sort in Agda. In Programming Languages-18th Brazilian Symposium, SBLP 2014, Maceio, Brazil, October 2-3, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8771 ), Fernando Magno Quint\u00e3o Pereira (Ed.). Springer, 62-76."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52335-9_47"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429094"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500587"},{"key":"e_1_2_1_27_1","volume-title":"Interactive Theorem Proving-9th International Conference, ITP","author":"Firsov Denis","year":"2018","unstructured":"Denis Firsov , Richard Blair , and Aaron Stump . 2018. Eficient Mendler-Style Lambda-Encodings in Cedille . In Interactive Theorem Proving-9th International Conference, ITP 2018 , Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 10895 ), Jeremy Avigad and Assia Mahboubi (Eds.). Springer , 235-252. Denis Firsov, Richard Blair, and Aaron Stump. 2018. Eficient Mendler-Style Lambda-Encodings in Cedille. In Interactive Theorem Proving-9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science, Vol. 10895 ), Jeremy Avigad and Assia Mahboubi (Eds.). Springer, 235-252."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018","author":"Firsov Denis","year":"2018","unstructured":"Denis Firsov and Aaron Stump . 2018 . Generic derivation of induction for impredicative encodings in Cedille . In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018 , Los Angeles, CA, USA , January 8-9, 2018, June Andronick and Amy P. Felty (Eds.). ACM, 215-227. Denis Firsov and Aaron Stump. 2018. Generic derivation of induction for impredicative encodings in Cedille. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, June Andronick and Amy P. Felty (Eds.). ACM, 215-227."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"volume-title":"A Categorical Programming Language. Ph. D. Dissertation","author":"Hagino Tatsuya","key":"e_1_2_1_30_1","unstructured":"Tatsuya Hagino . 1987. A Categorical Programming Language. Ph. D. Dissertation . University of Edinburgh. Tatsuya Hagino. 1987. A Categorical Programming Language. Ph. D. Dissertation. University of Edinburgh."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003378"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_1_33_1","unstructured":"Joomy Korkut Maksim Trifunovski and Daniel Licata. 2016. Intrinsic Verification of a Regular Expression Matcher. Unpublished available from Licata's web site.  \t\t\t\t  Joomy Korkut Maksim Trifunovski and Daniel Licata. 2016. Intrinsic Verification of a Regular Expression Matcher. Unpublished available from Licata's web site."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9157-2"},{"volume-title":"Theorem Proving in Higher Order Logics","author":"Krsti\u0107 Sava","key":"e_1_2_1_35_1","unstructured":"Sava Krsti\u0107 and John Matthews . 2003. Inductive Invariants for Nested Recursion . In Theorem Proving in Higher Order Logics , David Basin and Burkhart Wolf (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 253-269. Sava Krsti\u0107 and John Matthews. 2003. Inductive Invariants for Nested Recursion. In Theorem Proving in Higher Order Logics, David Basin and Burkhart Wolf (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 253-269."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_37_1","unstructured":"Standard library Coq. 2009. Sorting\/Mergesort.v.  \t\t\t\t  Standard library Coq. 2009. Sorting\/Mergesort.v."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900731X"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_6"},{"key":"e_1_2_1_40_1","unstructured":"The Agda development team. 2016. Agda. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki. php Version 2.5.1.  \t\t\t\t  The Agda development team. 2016. Agda. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki. php Version 2.5.1."},{"key":"e_1_2_1_41_1","unstructured":"The Coq development team. 2016. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria. fr Version 8.5.  \t\t\t\t  The Coq development team. 2016. The Coq proof assistant reference manual. LogiCal Project. http:\/\/coq.inria. fr Version 8.5."},{"key":"e_1_2_1_42_1","volume-title":"International Workshop, TYPES 2000","author":"McBride Conor","year":"2002","unstructured":"Conor McBride . 2002 . Elimination with a Motive. In Types for Proofs and Programs , International Workshop, TYPES 2000 , Durham, UK , December 8-12, 2000, Selected Papers (Lecture Notes in Computer Science, Vol. 2277 ), Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack (Eds.). Springer, 197-216. Conor McBride. 2002. Elimination with a Motive. In Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers (Lecture Notes in Computer Science, Vol. 2277 ), Paul Callaghan, Zhaohui Luo, James McKinna, and Robert Pollack (Eds.). Springer, 197-216."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","DOI":"10.1016\/0168-0072(91)90069-X","article-title":"Inductive types and type constraints in the second-order lambda calculus","volume":"51","author":"Mendler N. P.","year":"1991","unstructured":"N. P. Mendler . 1991 . Inductive types and type constraints in the second-order lambda calculus . Annals of Pure and Applied Logic 51 , 1 ( 1991 ), 159-172. N. P. Mendler. 1991. Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic 51, 1 ( 1991 ), 159-172.","journal-title":"Annals of Pure and Applied Logic"},{"key":"e_1_2_1_44_1","unstructured":"Neil Mitchell. 2021. Data.List.Extra. https:\/\/hackage.haskell.org\/package\/extra-1.7.10\/docs\/Data-List-Extra.html  \t\t\t\t  Neil Mitchell. 2021. Data.List.Extra. https:\/\/hackage.haskell.org\/package\/extra-1.7.10\/docs\/Data-List-Extra.html"},{"volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias","key":"e_1_2_1_45_1","unstructured":"Tobias Nipkow , Lawrence C Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : a proof assistant for higher-order logic . Vol. 2283 . Springer Science & Business Media . Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business Media."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-008-9038-0"},{"volume-title":"Handbook of Data Compression","author":"Salomon David","key":"e_1_2_1_47_1","unstructured":"David Salomon and Giovanni Motta . 2009. Handbook of Data Compression . Springer . David Salomon and Giovanni Motta. 2009. Handbook of Data Compression. Springer."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_16"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409004"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.75"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60675-0_35"},{"key":"e_1_2_1_55_1","first-page":"3","article-title":"Mendler-style Inductive Types, Categorically","volume":"6","author":"Uustalu Tarmo","year":"1999","unstructured":"Tarmo Uustalu and Varmo Vene . 1999 . Mendler-style Inductive Types, Categorically . Nordic J. of Computing 6 , 3 (Sept. 1999 ), 343-361. Tarmo Uustalu and Varmo Vene. 1999. Mendler-style Inductive Types, Categorically. Nordic J. of Computing 6, 3 (Sept. 1999 ), 343-361.","journal-title":"Nordic J. of Computing"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.02.020"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019916231463"},{"key":"e_1_2_1_58_1","volume-title":"The Eighth International Workshop on Coq for Programming Languages.","author":"Ye Qianchuan","year":"2022","unstructured":"Qianchuan Ye and Benjamin Delaware . 2022 . Scrap your boilerplate definitions in 10 lines of Ltac! . In The Eighth International Workshop on Coq for Programming Languages. Qianchuan Ye and Benjamin Delaware. 2022. Scrap your boilerplate definitions in 10 lines of Ltac!. In The Eighth International Workshop on Coq for Programming Languages."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571196","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571196","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571196"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":58,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571196"],"URL":"https:\/\/doi.org\/10.1145\/3571196","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}