{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:46Z","timestamp":1780994686996,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":44,"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":"EUMSCA","award":["101106046"],"award-info":[{"award-number":["101106046"]}]},{"name":"NWO","award":["OCENW.M20.380,OCENW.M20.053"],"award-info":[{"award-number":["OCENW.M20.380,OCENW.M20.053"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705873","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"34-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Intrinsically Correct Sorting in Cubical Agda"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-5210-2873","authenticated-orcid":false,"given":"Cass","family":"Alexandru","sequence":"first","affiliation":[{"name":"RPTU Kaiserslautern-Landau, Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2030-8056","authenticated-orcid":false,"given":"Vikraman","family":"Choudhury","sequence":"additional","affiliation":[{"name":"University of Bologna, Bologna, Italy"},{"name":"Inria Sophia Antipolis, Valbonne, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1404-6232","authenticated-orcid":false,"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1146-4161","authenticated-orcid":false,"given":"Niels","family":"van der Weide","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"The Agda Team. 2024. Function Definitions : Dot Patterns \u2014 Agda 2.7.0.1 documentation. https:\/\/agda.readthedocs.io\/en\/v2.7.0.1\/language\/function-definitions.html##dot-patterns"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","unstructured":"Cass Alexandru Vikraman Choudhury Jurriaan Rot and Niels van der Weide. 2024. Intrinsically Correct Sorting in Cubical Agda. https:\/\/doi.org\/10.5281\/zenodo.14279034 10.5281\/zenodo.14279034","DOI":"10.5281\/zenodo.14279034"},{"key":"e_1_3_2_2_3_1","volume-title":"Verified Functional Algorithms (1.5.5 ed.) (Software Foundations","author":"Appel Andrew","unstructured":"Andrew Appel. 2017. Verified Functional Algorithms (1.5.5 ed.) (Software Foundations, Vol. 3). https:\/\/softwarefoundations.cis.upenn.edu\/vfa-1.5.5\/"},{"key":"e_1_3_2_2_4_1","unstructured":"Bob Atkey. 2013. Typed DSLs for Sorting. https:\/\/github.com\/bobatkey\/sorting-types"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004501"},{"key":"e_1_3_2_2_6_1","volume-title":"Bird and Oege de Moor","author":"Richard","year":"1997","unstructured":"Richard S. Bird and Oege de Moor. 1997. Algebra of Programming. Prentice Hall. isbn:978-0-13-507245-5"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/645902.672777"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290314"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.10492"},{"key":"e_1_3_2_2_10_1","first-page":"3127","article-title":"Cubical Type Theory","volume":"4","author":"Cohen Cyril","year":"2017","unstructured":"Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2017. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. FLAP, 4, 10 (2017), 3127\u20133170. isbn:978-1-84890-268-8 http:\/\/www.collegepublications.co.uk\/downloads\/ifcolog00019.pdf","journal-title":"A Constructive Interpretation of the Univalence Axiom. FLAP"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_11"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9426-4"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167085"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628138"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022272"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364394.2364405"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_3_2_2_19_1","unstructured":"JetBrains Research. 2021. Universes \u2013 Arend Theorem Prover documentation. https:\/\/arend-lang.github.io\/documentation\/language-reference\/expressions\/universes.html"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.023"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2021.21"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-99-8311-7_7"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80350-0"},{"key":"e_1_3_2_2_24_1","unstructured":"Sandy Maguire. 2018. Higher-Kinded Data. https:\/\/reasonablypolymorphic.com\/blog\/higher-kinded-data\/"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48167-2_12"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.1984.0073"},{"key":"e_1_3_2_2_27_1","unstructured":"Conor McBride. 2011. Ornamental Algebras Algebraic Ornaments. https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/pub\/OAAO\/Ornament.pdf"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628163"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211391"},{"key":"e_1_3_2_2_31_1","unstructured":"Tobias Nipkow Jasmin Blanchette Manuel Eberl Alejandro G\u00f3mez-Londo\u00f1o Peter Lammich Christian Sternagel Simon Wimmer and Bohua Zhan. 2021. Functional Algorithms Verified!. https:\/\/www21.in.tum.de\/teaching\/fds\/SS21\/assets\/book-draft.pdf"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","unstructured":"Stefano Piceghello. 2020. Coherence for Monoidal Groupoids in HoTT. In DROPS-IDN\/v2\/Document\/10.4230\/LIPIcs.TYPES.2019.8. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik. https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2019.8 10.4230\/LIPIcs.TYPES.2019.8","DOI":"10.4230\/LIPIcs.TYPES.2019.8"},{"key":"e_1_3_2_2_33_1","volume-title":"Coherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theory","author":"Piceghello Stefano","unstructured":"Stefano Piceghello. 2021. Coherence for Monoidal and Symmetric Monoidal Groupoids in Homotopy Type Theory. The University of Bergen. isbn:9788230847114 https:\/\/bora.uib.no\/bora-xmlui\/handle\/11250\/2830640"},{"key":"e_1_3_2_2_34_1","unstructured":"Andrew M. Pitts. 2020. The combination of Cubical Agda with inductive families is logically inconsistent \u00b7 Issue #4606 \u00b7 agda\/agda. https:\/\/github.com\/agda\/agda\/issues\/4606"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000553"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:9)2013"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1137\/0211062"},{"key":"e_1_3_2_2_38_1","volume-title":"Practical Foundations of Mathematics","author":"Taylor Paul","unstructured":"Paul Taylor. 1999. Practical Foundations of Mathematics (Cambridge Studies in Advanced Mathematics). Cambridge University Press, Cambridge. isbn:978-0-521-63107-5 lccn:510"},{"key":"e_1_3_2_2_39_1","unstructured":"The agda\/cubical development team. 2018\/. The Agda\/Cubical Library. https:\/\/github.com\/agda\/cubical\/"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60675-0_35"},{"key":"e_1_3_2_2_42_1","volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","author":"Foundations Program The Univalent","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. https:\/\/homotopytypetheory.org\/book"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.3176\/phys.math.1998.3.01"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341691"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Denver CO USA","acronym":"CPP '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"]},"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.3705873","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705873","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.3705873"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":44,"alternative-id":["10.1145\/3703595.3705873","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705873","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"}}]}}