{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:23Z","timestamp":1750309523186,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"European Research Council (ERC)","award":["Horizon 2020 research and innovation programme (grant agreement No. 101001995)"],"award-info":[{"award-number":["Horizon 2020 research and innovation programme (grant agreement No. 101001995)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705885","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"214-230","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Machine Checked Proofs and Programs in Algebraic Combinatorics"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7531-5985","authenticated-orcid":false,"given":"Florent","family":"Hivert","sequence":"first","affiliation":[{"name":"University Paris-Saclay, Orsay, France"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60114-7_2"},{"key":"e_1_3_2_2_2_1","volume-title":"https:\/\/sites.math.rutgers.edu\/~asbuch\/lrcalc\/ Accessed on 09 04","author":"Buch Anders","year":"2024","unstructured":"Anders Buch. 2021-01-27. Littlewood-Richardson Calculator. https:\/\/sites.math.rutgers.edu\/~asbuch\/lrcalc\/ Accessed on 09 04, 2024"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854075"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.34"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218196702001139"},{"key":"e_1_3_2_2_6_1","unstructured":"Manuel Eberl. 2018. Symmetric Polynomials. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/Symmetric_Polynomials.html"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","unstructured":"P. Erd\u00f6s and G. Szeckeres. 1987. A Combinatorial Problem in Geometry. Birkh\u00e4user Boston Boston MA. 49\u201356. isbn:978-0-8176-4842-8 https:\/\/doi.org\/10.1007\/978-0-8176-4842-8_3 10.1007\/978-0-8176-4842-8_3","DOI":"10.1007\/978-0-8176-4842-8_3"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626241"},{"volume-title":"The Four Colour Theorem: Engineering of a Formal Proof","author":"Gonthier Georges","key":"e_1_3_2_2_9_1","unstructured":"Georges Gonthier. 2008. The Four Colour Theorem: Engineering of a Formal Proof. In Computer Mathematics, Deepak Kapur (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 333\u2013333. isbn:978-3-540-87827-8"},{"key":"e_1_3_2_2_10_1","volume-title":"Assia Mahboubi, Russell O\u2019Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Th\u00e9ry.","author":"Gonthier Georges","year":"2013","unstructured":"Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Fran\u00e7ois Garillot, St\u00e9phane Le Roux, Assia Mahboubi, Russell O\u2019Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Th\u00e9ry. 2013. A Machine-Checked Proof of the Odd Order Theorem. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 163\u2013179. isbn:978-3-642-39634-2"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(74)90031-0"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(79)90023-9"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5802\/crmath.468"},{"key":"e_1_3_2_2_14_1","unstructured":"Johan Commelin Hanting Zhang. 2020. Symmetric Polynomials and Elementary Symmetric Polynomials. https:\/\/leanprover-community.github.io\/mathlib_docs\/ring_theory\/mv_polynomial\/symmetric.html"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.01.012"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-017-0158-y"},{"volume-title":"The Representation Theory of the Symmetric Group","author":"James Gordon","key":"e_1_3_2_2_17_1","unstructured":"Gordon James and Adalbert Kerber. 1984. The Representation Theory of the Symmetric Group. Cambridge University Press."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1970.34.709"},{"key":"e_1_3_2_2_19_1","first-page":"1055","article-title":"The honeycomb model of _n() tensor products I: proof of the saturation conjecture","volume":"12","author":"Knutson Allen","year":"1999","unstructured":"Allen Knutson and Terence Tao. 1999. The honeycomb model of _n() tensor products I: proof of the saturation conjecture. J. AMS, 12, 4 (1999), 1055\u20131091.","journal-title":"J. AMS"},{"volume-title":"Algebraic Combinatoric on Words","author":"Lascoux Alain","key":"e_1_3_2_2_20_1","unstructured":"Alain Lascoux, B. Leclerc, and Jean-Yves Thibon. 2002. The Plactic Monoid. In Algebraic Combinatoric on Words, Lothaire M. (Ed.). Cambridge University Press, 164\u2013196. https:\/\/hal-upec-upem.archives-ouvertes.fr\/hal-00622651 incollection"},{"volume-title":"Symmetric functions and Hall polynomials","author":"Macdonald I. G.","key":"e_1_3_2_2_21_1","unstructured":"I. G. Macdonald. 1995. Symmetric functions and Hall polynomials (second ed.). The Clarendon Press Oxford University Press, New York. isbn:0-19-853489-2 With contributions by A. Zelevinsky, Oxford Science Publications"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2022. Mathematical Components. https:\/\/doi.org\/10.5281\/ZENODO.3999478 10.5281\/ZENODO.3999478","DOI":"10.5281\/ZENODO.3999478"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10801-011-0325-1"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1137\/S009753970038715X"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10801-006-0008-5"},{"key":"e_1_3_2_2_26_1","volume-title":"Combinatorial Algorithms, and Symmetric Functions","author":"Sagan Bruce E.","year":"1991","unstructured":"Bruce E. Sagan. 2001. The Symmetric Group: Representations, Combinatorial Algorithms, and Symmetric Functions (2nd ed.) (Graduate Texts in Mathematics, Vol. 203). Springer-Verlag, New York. isbn:0-387-95067-2 First edition published by Wadsworth & Brooks\/Cole Advanced Books & Software, 1991.","edition":"2"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1961-015-3"},{"volume-title":"Combinatoire et Repr\u00e9sentation du Groupe Sym\u00e9trique","author":"Sch\u00fctzenberger M.-P.","key":"e_1_3_2_2_28_1","unstructured":"M.-P. Sch\u00fctzenberger. 1977. La correspondance de Robinson. In Combinatoire et Repr\u00e9sentation du Groupe Sym\u00e9trique, Dominique Foata (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 59\u2013113. isbn:978-3-540-37385-8"},{"key":"e_1_3_2_2_29_1","unstructured":"W. A. Stein. 2018. Sage Mathematics Software. http:\/\/www.sagemath.org"},{"key":"e_1_3_2_2_30_1","volume-title":"A concise proof of the Littlewood-Richardson rule.. The Electronic Journal of Combinatorics [electronic only], 9, 1","author":"Stembridge John R.","year":"2002","unstructured":"John R. Stembridge. 2002. A concise proof of the Littlewood-Richardson rule.. The Electronic Journal of Combinatorics [electronic only], 9, 1 (2002), Research paper N5, 4 p.\u2013Research paper N5, 4 p.. http:\/\/eudml.org\/doc\/121943"},{"key":"e_1_3_2_2_31_1","first-page":"1055","article-title":"Book review of The representation theory of the symmetric group, by Gordon James and Adalbert","volume":"8","author":"Towber Jacob","year":"1983","unstructured":"Jacob Towber. 1983. Book review of The representation theory of the symmetric group, by Gordon James and Adalbert Kerber. Bull. AMS, 8, 2 (1983), 1055\u20131091.","journal-title":"Kerber. Bull. AMS"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.2969\/msjmemoirs"},{"key":"e_1_3_2_2_33_1","volume-title":"https:\/\/www.cs.ru.nl\/~freek\/100\/ Accessed on 09 04","author":"Wiedijk Freek","year":"2024","unstructured":"Freek Wiedijk. 2024-06-13. Formalizing 100 Theorems. https:\/\/www.cs.ru.nl\/~freek\/100\/ Accessed on 09 04, 2024"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1088\/0953-4075"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0021-8693(81)90128-9"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"location":"Denver CO USA","acronym":"CPP '25"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705885","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705885","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705885"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":35,"alternative-id":["10.1145\/3703595.3705885","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705885","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}