{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T08:49:27Z","timestamp":1758703767287,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":34,"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\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705883","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"187-197","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalized Burrows-Wheeler Transform"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3530-6662","authenticated-orcid":false,"given":"Louis","family":"Cheung","sequence":"first","affiliation":[{"name":"The University of Melbourne, Melbourne, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6638-0232","authenticated-orcid":false,"given":"Alistair","family":"Moffat","sequence":"additional","affiliation":[{"name":"The University of Melbourne, Melbourne, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4785-2836","authenticated-orcid":false,"given":"Christine","family":"Rizkallah","sequence":"additional","affiliation":[{"name":"The University of Melbourne, Melbourne, Australia"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_2_1_1","DOI":"10.4230\/LIPICS.ITP.2019.5"},{"doi-asserted-by":"publisher","unstructured":"Y. Bertot and P. Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Springer. https:\/\/doi.org\/10.1007\/978-3-662-07964-5 10.1007\/978-3-662-07964-5","key":"e_1_3_2_2_2_1","DOI":"10.1007\/978-3-662-07964-5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_3_1","DOI":"10.1017\/S0956796804005118"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_4_1","DOI":"10.1007\/s10009-014-0314-5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_5_1","DOI":"10.1007\/s10009-013-0293-y"},{"unstructured":"M. Burrows and D. Wheeler. 1994. A Block-Sorting Lossless Data Compression Algorithm. Digital SRC Research Report.","key":"e_1_3_2_2_6_1"},{"doi-asserted-by":"publisher","unstructured":"L. Cheung and C. Rizkallah. 2024. Formalized Burrows-Wheeler Transform (Artefact). https:\/\/doi.org\/10.5281\/zenodo.14279882 10.5281\/zenodo.14279882","key":"e_1_3_2_2_7_1","DOI":"10.5281\/zenodo.14279882"},{"unstructured":"L. Cheung and C. Rizkallah. 2024. Formally Verified Suffix Array Construction. Archive of Formal Proofs September issn:2150-914x https:\/\/isa-afp.org\/entries\/SuffixArray.html","key":"e_1_3_2_2_8_1"},{"doi-asserted-by":"crossref","unstructured":"M. Crochemore C. Hancart and T. Lecroq. 2007. Algorithms on Strings. Cambridge University Press Cambridge. isbn:978-0-521-84899-2","key":"e_1_3_2_2_9_1","DOI":"10.1017\/CBO9780511546853"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_10_1","DOI":"10.1016\/J.TCS.2014.03.014"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_11_1","DOI":"10.1007\/s10009-014-0308-3"},{"doi-asserted-by":"publisher","unstructured":"P. Ferragina and G. Manzini. 2000. Opportunistic Data Structures with Applications. In Foundations of Computer Science. IEEE Computer Society 390\u2013398. https:\/\/doi.org\/10.1109\/SFCS.2000.892127 10.1109\/SFCS.2000.892127","key":"e_1_3_2_2_12_1","DOI":"10.1109\/SFCS.2000.892127"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_13_1","DOI":"10.1145\/1082036.1082039"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_14_1","DOI":"10.1016\/J.TCS.2007.07.019"},{"doi-asserted-by":"crossref","unstructured":"M. Gordon R. Milner and C. P. Wadsworth. 1979. Edinburgh LCF: A Mechanised Logic of Computation (Lecture Notes in Computer Science Vol. 78). Springer.","key":"e_1_3_2_2_15_1","DOI":"10.1007\/3-540-09724-4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_16_1","DOI":"10.1007\/3-540-45061-0_73"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_17_1","DOI":"10.1016\/j.jda.2004.08.002"},{"key":"e_1_3_2_2_18_1","volume-title":"Proc. Prague Stringtology. Prague Stringology Club, Department of Computer Science and Engineering","author":"Kufleitner M.","year":"2009","unstructured":"M. Kufleitner. 2009. On Bijective Variants of the Burrows-Wheeler Transform. In Proc. Prague Stringtology. Prague Stringology Club, Department of Computer Science and Engineering, Faculty of Electrical Engineering, Czech Technical University in Prague, 65\u201379. http:\/\/www.stringology.org\/event\/2009\/p07.html"},{"doi-asserted-by":"publisher","unstructured":"B. Langmead and S. L. Salzberg. 2012. Fast Gapped-Read Alignment with Bowtie 2. Nature Methods 9 4 (2012) 01 Apr 357\u2013359. https:\/\/doi.org\/10.1038\/nmeth.1923 10.1038\/nmeth.1923","key":"e_1_3_2_2_19_1","DOI":"10.1038\/nmeth.1923"},{"doi-asserted-by":"publisher","unstructured":"B. Langmead C. Trapnell M. Pop and S. L. Salzberg. 2009. Ultrafast and Memory-efficient Alignment of Short DNA Sequences to the Human Genome. Genome Biology 10 3 (2009) 04 Mar 25. https:\/\/doi.org\/10.1186\/gb-2009-10-3-r25 10.1186\/gb-2009-10-3-r25","key":"e_1_3_2_2_20_1","DOI":"10.1186\/gb-2009-10-3-r25"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_21_1","DOI":"10.1093\/bioinformatics"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_22_1","DOI":"10.1093\/bioinformatics"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_23_1","DOI":"10.1137\/0222058"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_24_1","DOI":"10.1145\/382780.382782"},{"doi-asserted-by":"crossref","unstructured":"A. Moffat and A. Turpin. 2002. Compression and Coding Algorithms. Kluwer Academic Publishers Boston MA.","key":"e_1_3_2_2_25_1","DOI":"10.1007\/978-1-4615-0935-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_26_1","DOI":"10.1016\/J.JDA.2013.07.004"},{"volume-title":"Compact Data Structures - A Practical Approach","author":"Navarro G.","unstructured":"G. Navarro. 2016. Compact Data Structures - A Practical Approach. Cambridge University Press, Cambridge. isbn:978-1-10-715238-0","key":"e_1_3_2_2_27_1"},{"doi-asserted-by":"publisher","unstructured":"T. Nipkow and G. Klein. 2014. Concrete Semantics - With Isabelle\/HOL. Springer Berlin Heidelberg. https:\/\/doi.org\/10.1007\/978-3-319-10542-0 10.1007\/978-3-319-10542-0","key":"e_1_3_2_2_28_1","DOI":"10.1007\/978-3-319-10542-0"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_29_1","DOI":"10.1007\/3-540-45949-9"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_30_1","DOI":"10.1109\/DCC.2009.42"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_31_1","DOI":"10.1109\/TC.2010.188"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_32_1","DOI":"10.1007\/978-3-642-39053-1_42"},{"unstructured":"J. Seward. 1996. bzip2 Homepage. https:\/\/sourceware.org\/bzip2\/index.html Accessed: 2023-09-12","key":"e_1_3_2_2_33_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_2_34_1","DOI":"10.1007\/978-3-319-47846-3_16"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"acronym":"CPP '25","name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Denver CO USA"},"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.3705883","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705883","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.3705883"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":34,"alternative-id":["10.1145\/3703595.3705883","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705883","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"}}]}}