{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:42:29Z","timestamp":1767926549078,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Swedish Research Council","award":["2019-04545"],"award-info":[{"award-number":["2019-04545"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575677","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"239-252","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Computing Cohomology Rings in Cubical Agda"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Lamiaux","sequence":"first","affiliation":[{"name":"University of Paris-Saclay, France \/ ENS Paris-Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Ljungstr\u00f6m","sequence":"additional","affiliation":[{"name":"Stockholm University, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[{"name":"Stockholm University, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434293"},{"key":"e_1_3_2_1_2_1","volume-title":"The cup product on cohomology groups in Homotopy Type Theory. Master\u2019s thesis","author":"Baumann Tim","unstructured":"Tim Baumann. 2018. The cup product on cohomology groups in Homotopy Type Theory. Master\u2019s thesis. University of Augsburg."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.2307\/1970209"},{"key":"e_1_3_2_1_4_1","unstructured":"Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. Ph. D. Dissertation. Universit\u00e9 Nice Sophia Antipolis. arxiv:1606.05916"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.11"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209188"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330081"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108975704"},{"key":"e_1_3_2_1_9_1","volume-title":"Synthetic Cohomology in Homotopy Type Theory. Master\u2019s thesis","author":"Cavallo Evan","unstructured":"Evan Cavallo. 2015. Synthetic Cohomology in Homotopy Type Theory. Master\u2019s thesis. Carnegie Mellon University."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2015.5"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209197"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_21"},{"key":"e_1_3_2_1_14_1","volume-title":"Foundations of Algebraic Topology","author":"Eilenberg Samuel","unstructured":"Samuel Eilenberg and Norman Steenrod. 1952. Foundations of Algebraic Topology. Princeton University Press. isbn:9780608102351"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167085"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_1_18_1","unstructured":"Allen Hatcher. 2002. Algebraic Topology. Cambridge University Press. isbn:9780521795401 https:\/\/pi.math.cornell.edu\/~hatcher\/AT\/AT.pdf"},{"key":"e_1_3_2_1_19_1","volume-title":"The Art of Computer Programming, Volume 2: Seminumerical Algorithms","author":"Knuth Donald E.","year":"2010","unstructured":"Donald E. Knuth. 1981. The Art of Computer Programming, Volume 2: Seminumerical Algorithms. Addison-Wesley. isbn:0201038226"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_3_2_1_22_1","volume-title":"The Buchberger Algorithm as a Tool for Ideal Theory of Polynomial Rings in Constructive Mathematics","author":"Lombardi Henri","unstructured":"Henri Lombardi and Herv\u00e9 Perdry. 1998. The Buchberger Algorithm as a Tool for Ideal Theory of Polynomial Rings in Constructive Mathematics. In Gr\u00f6bner Bases and Applications, Bruno Buchberger and Franz Winkler (Eds.). Cambridge University Press, 393\u2013407. isbn:9780511565847"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_3_2_1_24_1","volume-title":"Intuitionistic type theory (Studies in Proof Theory","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory (Studies in Proof Theory, Vol. 1). Bibliopolis. isbn:88-7088-105-9"},{"key":"e_1_3_2_1_25_1","volume-title":"A Course in Constructive Algebra","author":"Mines Ray","unstructured":"Ray Mines, Fred Richman, and Wim Ruitenburg. 1988. A Course in Constructive Algebra. Springer-Verlag."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373825"},{"key":"e_1_3_2_1_27_1","unstructured":"Michael Shulman. 2013. Cohomology. post on the Homotopy Type Theory blog: http:\/\/homotopytypetheory.org\/2013\/07\/24\/"},{"key":"e_1_3_2_1_28_1","unstructured":"The Development Team. 2022. The Programming Language. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"e_1_3_2_1_29_1","unstructured":"The Mathlib Development Team. 2022. The Mathlib. https:\/\/github.com\/leanprover-community\/mathlib\/"},{"key":"e_1_3_2_1_30_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Self-published, Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_3_2_1_31_1","volume-title":"On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. Ph. D. Dissertation","author":"van Doorn Floris","year":"1808","unstructured":"Floris van Doorn. 2018. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. Ph. D. Dissertation. Carnegie Mellon University. arxiv:1808.10690"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000034"},{"key":"e_1_3_2_1_33_1","unstructured":"Vladimir Voevodsky. 2010. The equivalence axiom and univalent models of type theory. http:\/\/www.math.ias.edu\/vladimir\/files\/CMU_talk.pdf Notes from a talk at Carnegie Mellon University"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Boston MA USA","acronym":"CPP '23","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575677","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575677","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575677"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":33,"alternative-id":["10.1145\/3573105.3575677","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575677","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}