{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:12:48Z","timestamp":1775671968184,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","funder":[{"name":"ANR NARCO","award":["ANR-21-CE48-0011"],"award-info":[{"award-number":["ANR-21-CE48-0011"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779103","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"15-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Bar Inductive Predicates for Constructive Algebra in Rocq"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9860-7203","authenticated-orcid":false,"given":"Dominique","family":"Larchey-Wendling","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Lorraine, Vandoeuvre-l\u00e8s-Nancy, France"},{"name":"CNRS, Vandoeuvre-l\u00e8s-Nancy, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854072"},{"key":"e_1_3_2_1_2_1","volume-title":"Mathematical Logic and Theoretical Computer Science. Taylor&Francis","author":"Blass A.","unstructured":"A. Blass. 1986. Well-Ordering and Induction in Intuitionistic Logic and Topoi. In Mathematical Logic and Theoretical Computer Science. Taylor&Francis Group, Boca Raton. 29\u201348."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","unstructured":"G. Buriola P. Schuster and I. Blechschmidt. 2023. A Constructive Picture of\u00a0Noetherian Conditions and\u00a0Well Quasi-orders. In Unity of Logic and Computation (CiE 2023). Springer Cham. 50\u201362. isbn:978-3-031-36978-0 https:\/\/doi.org\/10.1007\/978-3-031-36978-0_5 10.1007\/978-3-031-36978-0_5","DOI":"10.1007\/978-3-031-36978-0_5"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_2_1_5_1","volume-title":"About Brouwer\u2019s Fan Theorem. Revue internationale de philosophie, 58, 230 (4)","author":"Coquand T.","year":"2004","unstructured":"T. Coquand. 2004. About Brouwer\u2019s Fan Theorem. Revue internationale de philosophie, 58, 230 (4) (2004), 483\u2013489. http:\/\/www.jstor.org\/stable\/23955601"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","unstructured":"T. Coquand A. M\u00f6rtberg and V. Siles. 2012. Coherent and Strongly Discrete Rings in Type Theory. In Certified Programs and Proofs (CPP 2012). Springer Berlin Heidelberg 273\u2013288. isbn:978-3-642-35308-6 https:\/\/doi.org\/10.1007\/978-3-642-35308-6_21 10.1007\/978-3-642-35308-6_21","DOI":"10.1007\/978-3-642-35308-6_21"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"T. Coquand and H. Persson. 1999. Gr\u00f6bner Bases in Type Theory. In Types for Proofs and Programs (TYPES \u201998). Springer Berlin Heidelberg 33\u201346. isbn:978-3-540-48167-6 https:\/\/doi.org\/10.1007\/3-540-48167-2_3 10.1007\/3-540-48167-2_3","DOI":"10.1007\/3-540-48167-2_3"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097789"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48167-2_7"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"G. Gonthier A. Asperti J. Avigad Y. Bertot C. Cohen F. Garillot S. Le Roux A. Mahboubi R. O\u2019Connor S. O. Biha I. Pasca L. Rideau A. Solovyev E. Tassi and L. Th\u00e9ry. 2013. A Machine-Checked Proof of the Odd Order Theorem. In Interactive Theorem Proving (ITP 2013). Springer Berlin Heidelberg 163\u2013179. isbn:9783642396335 https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14 10.1007\/978-3-642-39634-2_14","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","unstructured":"B. Gr\u00e9goire and A. Mahboubi. 2005. Proving Equalities in a Commutative Ring Done Right in Coq. In Theorem Proving in Higher Order Logics (TPHOLs 2005). Springer Berlin Heidelberg 98\u2013113. isbn:978-3-540-31820-0 https:\/\/doi.org\/10.1007\/11541868_7 10.1007\/11541868_7","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01208503"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80154-X"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"T. Lamiaux A. Ljungstr\u00f6m and A. M\u00f6rtberg. 2023. Computing Cohomology Rings in Cubical Agda. In Certified Programs and Proofs (CPP 2023). Association for Computing Machinery New York NY USA. 239\u2013252. isbn:9798400700262 https:\/\/doi.org\/10.1145\/3573105.3575677 10.1145\/3573105.3575677","DOI":"10.1145\/3573105.3575677"},{"key":"e_1_3_2_1_15_1","unstructured":"D. Larchey-Wendling. 2024. The Coq-Kruskal project. https:\/\/github.com\/DmxLarchey\/Coq-Kruskal"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2024.2"},{"key":"e_1_3_2_1_17_1","unstructured":"E. Makarov et al. 2006. Constructive Coq Repository at Nijmegen. https:\/\/github.com\/rocq-community\/corn"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2003.02.001"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200710042"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000509"},{"key":"e_1_3_2_1_21_1","unstructured":"H. Persson. 2001. An Integrated Development of Buchberger\u2019s Algorithm in Coq. INRIA. https:\/\/inria.hal.science\/inria-00072316"},{"key":"e_1_3_2_1_22_1","unstructured":"B. Puyobro B. Ballenghien and B. Wolff. 2025. A Proof of Hilbert Basis Theorem and an Extension to Formal Power Series. Archive of Formal Proofs issn:2150-914x https:\/\/isa-afp.org\/entries\/Hilbert_Basis.html"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.2307\/2040452"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jalgebra.2025.03.027"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02925651"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1574"},{"key":"e_1_3_2_1_27_1","volume-title":"Algorithm. In Conference on Automated Deduction (CADE-15)","author":"Th\u00e9ry L.","year":"1998","unstructured":"L. Th\u00e9ry. 1998. A Certified Version of Buchberger\u2019s Algorithm. In Conference on Automated Deduction (CADE-15). Springer Berlin Heidelberg, 349\u2013364. isbn:3540646752 https:\/\/dl.acm.org\/doi\/10.5555\/648234.753471"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1026518331905"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","unstructured":"W. Veldman. 2006. Brouwer\u2019s Real Thesis on Bars. Philosophia Scienti\u00e6 21\u201342. https:\/\/doi.org\/10.4000\/philosophiascientiae.404","DOI":"10.4000\/philosophiascientiae.404"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","unstructured":"D. Vytiniotis T. Coquand and D. Wahlstedt. 2012. Stop When You Are Almost-Full. In Interactive Theorem Proving (ITP 2012). Springer Berlin Heidelberg 250\u2013265. isbn:978-3-642-32347-8 https:\/\/doi.org\/10.1007\/978-3-642-32347-8_17 10.1007\/978-3-642-32347-8_17","DOI":"10.1007\/978-3-642-32347-8_17"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:54:30Z","timestamp":1775667270000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":30,"alternative-id":["10.1145\/3779031.3779103","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779103","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}