{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,24]],"date-time":"2026-09-24T15:19:18Z","timestamp":1790263158858,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T00:00:00Z","timestamp":1720396800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,8]]},"DOI":"10.1145\/3661814.3662077","type":"proceedings-article","created":{"date-parts":[[2024,6,21]],"date-time":"2024-06-21T12:30:12Z","timestamp":1718973012000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Delooping cyclic groups with lens spaces in homotopy type theory"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0767-2569","authenticated-orcid":false,"given":"Samuel","family":"Mimram","sequence":"first","affiliation":[{"name":"LIX, \u00c9cole Polytechnique, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8398-2577","authenticated-orcid":false,"given":"Emile","family":"Oleon","sequence":"additional","affiliation":[{"name":"LIX, Ecole polytechnique, Palaiseau, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004108001783"},{"key":"e_1_3_2_1_2_1","unstructured":"Marc Bezem Ulrik Buchholtz Pierre Cagne Bj\u00f8rn Ian Dundas and Daniel R. Grayson. [n. d.]. Symmetry. https:\/\/github.com\/UniMath\/SymmetryBook."},{"key":"e_1_3_2_1_3_1","unstructured":"Guillaume Brunerie. 2016. On the homotopy groups of spheres in homotopy type theory. Ph. D. Dissertation. arXiv:1606.05916"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9468-2"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(2:7)2020"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005146"},{"key":"e_1_3_2_1_7_1","volume-title":"Delooping generated groups in homotopy type theory. (2024). Accepted at FSCD","author":"Champin Camil","year":"2024","unstructured":"Camil Champin, Samuel Mimram, and \u00c9mile Oleon. 2024. Delooping generated groups in homotopy type theory. (2024). Accepted at FSCD 2024."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9372-6"},{"key":"e_1_3_2_1_9_1","volume-title":"Algebraic topology","author":"Hatcher Allen","unstructured":"Allen Hatcher. 2009. Algebraic topology. Cambridge University Press."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4171\/JEMS\/1050"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129523000026"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603153"},{"key":"e_1_3_2_1_14_1","unstructured":"Saunders Mac Lane and Garrett Birkhoff. 1999. Algebra. Vol. 330. American Mathematical Society."},{"key":"e_1_3_2_1_15_1","unstructured":"Saunders MacLane. 2012. Homology. Springer Science & Business Media."},{"key":"e_1_3_2_1_16_1","volume-title":"Intuitionistic type theory","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Vol. 9. Bibliopolis Naples."},{"key":"e_1_3_2_1_17_1","volume-title":"A concise course in algebraic topology","author":"May J Peter","unstructured":"J Peter May. 1999. A concise course in algebraic topology. University of Chicago press."},{"key":"e_1_3_2_1_18_1","volume-title":"I. Annals of Mathematics","author":"Milnor John","year":"1956","unstructured":"John Milnor. 1956. Construction of universal bundles, I. Annals of Mathematics (1956), 272--284."},{"key":"e_1_3_2_1_19_1","volume-title":"II. Annals of Mathematics","author":"Milnor John","year":"1956","unstructured":"John Milnor. 1956. Construction of universal bundles, II. Annals of Mathematics (1956), 430--436."},{"key":"e_1_3_2_1_20_1","unstructured":"Henri Poincar\u00e9. 1895. Analysis situs. Gauthier-Villars Paris France."},{"key":"e_1_3_2_1_21_1","unstructured":"Egbert Rijke. 2017. The join construction. (2017). arXiv:1701.07538 Preprint."},{"key":"e_1_3_2_1_22_1","unstructured":"Egbert Rijke. 2018. Classifying Types. Ph. D. Dissertation. Carnegie Mellon University. arXiv:1906.09435"},{"key":"e_1_3_2_1_23_1","unstructured":"Thomas Streicher. 2018. Fibered categories \u00e0 la Jean Benabou. (2018). arXiv:1801.02927 Preprint."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01736688"},{"key":"e_1_3_2_1_25_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book, Institute for Advanced Study. arXiv:1308.0729"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"David W\u00e4rn. 2023. Eilenberg-MacLane spaces and stabilisation in homotopy type theory. (2023). arXiv:2301.03685 Preprint.","DOI":"10.1007\/s40062-023-00330-5"},{"key":"e_1_3_2_1_27_1","unstructured":"Matthew Watkins. 1990. A Short Survey of Lens Spaces. (1990). Undergraduate dissertation."}],"event":{"name":"LICS '24: 39th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Tallinn Estonia","acronym":"LICS '24","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","IEEE Computer Society","EACSL"]},"container-title":["Proceedings of the 39th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662077","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3661814.3662077","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:08Z","timestamp":1750290248000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3661814.3662077"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,8]]},"references-count":27,"alternative-id":["10.1145\/3661814.3662077","10.1145\/3661814"],"URL":"https:\/\/doi.org\/10.1145\/3661814.3662077","relation":{},"subject":[],"published":{"date-parts":[[2024,7,8]]},"assertion":[{"value":"2024-07-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}