{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:12:35Z","timestamp":1775671955504,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","funder":[{"name":"European Research Council","award":["101001995"],"award-info":[{"award-number":["101001995"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779101","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"128-142","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Certifying the Decidability of the Word Problem in Monoids at Large"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-1576","authenticated-orcid":false,"given":"Reinis","family":"Cirpons","sequence":"first","affiliation":[{"name":"Nantes Universit\u00e9 - \u00c9cole Centrale Nantes - CNRS - Inria - LS2N - UMR 6004, Nantes, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7531-5985","authenticated-orcid":false,"given":"Florent","family":"Hivert","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CNRS - ENS Paris Saclay - Inria - LMF, Gif-sur-Yvette, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0312-5461","authenticated-orcid":false,"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9 - \u00c9cole Centrale Nantes - CNRS - Inria - LS2N - UMR 6004, Nantes, France"},{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6697-1809","authenticated-orcid":false,"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CNRS - ENS Paris Saclay - Inria - LMF, Gif-sur-Yvette, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5489-1617","authenticated-orcid":false,"given":"James D.","family":"Mitchell","sequence":"additional","affiliation":[{"name":"St Andrews University, St Andrews, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1871-8910","authenticated-orcid":false,"given":"Finn","family":"Smith","sequence":"additional","affiliation":[{"name":"St Andrews University, St Andrews, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01158256"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/360825.360855"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575678"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000120"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_26"},{"key":"e_1_3_2_1_6_1","volume-title":"Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci","author":"Bolan Matthew","year":"2025","unstructured":"Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andr\u00e9s Goens, Aaron Hill, Harald Husum, Hern\u00e1n Ibarra Mejia, Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, J\u00e9r\u00e9my Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. 2025. The Equational Theories Project: Advancing collaborative mathematical research at scale. https:\/\/teorth.github.io\/equational_theories\/paper.pdf"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Reinis Cirpons Joseph Edwards James D. Mitchell Maria Tsalakou and Murray Whyte. 2025. libsemigroups_pybind11. https:\/\/doi.org\/10.5281\/zenodo.16814180 10.5281\/zenodo.16814180","DOI":"10.5281\/zenodo.16814180"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Reinis Cirpons James D. Mitchell and Finn Smith. 2025. Database of 1-relation monoid word problem decidability proofs. https:\/\/doi.org\/10.5281\/zenodo.17726031 10.5281\/zenodo.17726031","DOI":"10.5281\/zenodo.17726031"},{"key":"e_1_3_2_1_9_1","volume-title":"20th International Workshop on Termination. https:\/\/www.imn.htwk-leipzig.de\/WST2025\/proceedings\/WST2025_paper_16","author":"Cirpons Reinis","unstructured":"Reinis Cirpons, James D. Mitchell, and Finn L. Smith. 2025. Off with the head: termination provers and the word problem for 1-relation monoids. In 20th International Workshop on Termination. https:\/\/www.imn.htwk-leipzig.de\/WST2025\/proceedings\/WST2025_paper_16.pdf"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2011.21"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2307\/2032597"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2021.21"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94821-8_15"},{"key":"e_1_3_2_1_14_1","volume-title":"6th International Workshop on Coq for Programming Languages. https:\/\/popl20","author":"Forster Yannick","year":"2020","unstructured":"Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. 2020. A Coq library of undecidable problems. In 6th International Workshop on Coq for Programming Languages. https:\/\/popl20.sigplan.org\/details\/CoqPL-2020-papers\/5\/A-Coq-Library-of-Undecidable-Problems"},{"key":"e_1_3_2_1_15_1","unstructured":"Jo\u00ebl Gay. 2018. Representation of Monoids and Lattice Structures in the Combinatorics of Weyl Groups. Ph. D. Dissertation. Universit\u00e9 Paris-Saclay. https:\/\/theses.fr\/2018SACLS209"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0021-8693(79)90238-2"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972710000365"},{"key":"e_1_3_2_1_18_1","first-page":"1382","article-title":"Formal proof\u2013the four-color theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier. 2008. Formal proof\u2013the four-color theorem. Notices of the AMS, 55, 11 (2008), 1382\u20131393.","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11737414_8"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1090\/s0894-0347-08-00590-0"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Thomas Hales Mark Adams Gertrud Bauer Tat Dat Dang John Harrison Le Truong Hoang Cezary Kaliszyk Victor Magron Sean McLaughlin Tat Thang Nguyen Quang Truong Nguyen Tobias Nipkow Steven Obua Joseph Pleso Jason Rute Alexey Solovyev Thi Hoai An Ta Nam Trung Tran Thi Diep Trieu Josef Urban Ky Vu and Roland Zumkeller. 2017. A formal proof of the Kepler conjecture. Forum of Mathematics Pi 5 (2017) 29 pages. https:\/\/doi.org\/10.1017\/fmp.2017.1 10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v32i1.12209"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Florent Hivert Assia Mahboubi James Mitchell Guillaume Melquiond and Reinis Cirpons. 2025. hivert\/MonoidPresentation: CPP-2026. https:\/\/doi.org\/10.5281\/zenodo.17802630 10.5281\/zenodo.17802630","DOI":"10.5281\/zenodo.17802630"},{"key":"e_1_3_2_1_24_1","volume-title":"15th International Workshop on Termination, Aart Middeldorp and Ren\u00e9 Thiemann (Eds.). 90\u201390","author":"Hofbauer Dieter","year":"2016","unstructured":"Dieter Hofbauer. 2016. MultumNonMulta: System description. In 15th International Workshop on Termination, Aart Middeldorp and Ren\u00e9 Thiemann (Eds.). 90\u201390. http:\/\/cl-informatik.uibk.ac.at\/workspace\/events\/wst2016.pdf"},{"key":"e_1_3_2_1_25_1","volume-title":"KBMAG: Knuth-Bendix on Monoids and Automatic Groups. https:\/\/gap-packages.github.io\/kbmag\/ GAP package version 1.5.11","author":"Holt Derek","year":"2023","unstructured":"Derek Holt. 2023. KBMAG: Knuth-Bendix on Monoids and Automatic Groups. https:\/\/gap-packages.github.io\/kbmag\/ GAP package version 1.5.11"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.22"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jalgebra.2008.09.038"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01455888"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2020. Mathematical Components. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.3999478 10.5281\/zenodo.3999478","DOI":"10.5281\/zenodo.3999478"},{"key":"e_1_3_2_1_31_1","first-page":"555","article-title":"Simple examples of undecidable associative calculi","volume":"8","author":"Matiyasevich Yuri V.","year":"1967","unstructured":"Yuri V. Matiyasevich. 1967. Simple examples of undecidable associative calculi. Soviet Mathematics. Doklady, 8 (1967), 555\u2013557. issn:0197-6788","journal-title":"Soviet Mathematics. Doklady"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jalgebra.2023.04.019"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","unstructured":"James D. Mitchell Michael Young Finn Smith Reinis Cirpons Florent Hivert Jerry James Nicolas M. Thi\u00e9ry Joe Edwards Wilf Wilson Dima Pasechnik Isuru Fernando Jan Engelhardt Luke Elliott and Max Horn. 2023. libsemigroups\/libsemigroups: 2.7.0. https:\/\/doi.org\/10.5281\/ZENODO.7761055 10.5281\/ZENODO.7761055","DOI":"10.5281\/ZENODO.7761055"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s1-28.1.357"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00233-021-10216-8"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00233-022-10310-5"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15984-3_302"},{"key":"e_1_3_2_1_38_1","unstructured":"Slava Pestov. 2025. A two-relation monoid does not have finite derivation type. In preparation"},{"key":"e_1_3_2_1_39_1","unstructured":"John Hermann Remmers. 1971. Some algorithmic problems for semigroups: a geometric approach. Ph. D. Dissertation. USA. AAI7123856"},{"key":"e_1_3_2_1_40_1","volume-title":"Semigroup presentations. Ph. D. Dissertation","author":"Ru\u0161kuc Nikola","unstructured":"Nikola Ru\u0161kuc. 1995. Semigroup presentations. Ph. D. Dissertation. University of St Andrews. http:\/\/hdl.handle.net\/10023\/2821"},{"key":"e_1_3_2_1_41_1","volume-title":"Pavel Kropitz, Shawn Ligocki,  mxdys, Mateusz Na\u015bciszewski,  savask, Tristan St\u00e9rin, Chris Xu, Jason Yuen, and Th\u00e9o Zimmermann.","author":"Collaboration The","year":"2025","unstructured":"The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja K\u0105dzio\u0142 ka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Na\u015bciszewski, savask, Tristan St\u00e9rin, Chris Xu, Jason Yuen, and Th\u00e9o Zimmermann. 2025. Determination of the fifth Busy Beaver value. arxiv:2509.12337. https:\/\/bbchallenge.org\/"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_31"},{"key":"e_1_3_2_1_43_1","unstructured":"Laurent Th\u00e9ry. 2025. The CoqPrime Library. https:\/\/github.com\/thery\/coqprime"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_6"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_22"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9249-2"}],"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.3779101","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:54:26Z","timestamp":1775667266000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779101"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":46,"alternative-id":["10.1145\/3779031.3779101","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779101","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"}}]}}