{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:12:35Z","timestamp":1760044355102,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["NI 491\/16-1"],"award-info":[{"award-number":["NI 491\/16-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Stiftelsen f\u00f6r Strategisk Forskning"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373834","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"18-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Proof pearl: Braun trees"],"prefix":"10.1145","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[{"name":"TU Munich, Germany"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","year":"2009","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Clifford Stein . Introduction to Algorithms . MIT Press , 3 rd edition, 2009 . Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. MIT Press, 3rd edition, 2009.","edition":"3"},{"key":"e_1_3_2_1_2_1","first-page":"298","volume-title":"Western Joint Computer Conference, IRE-AIEE-ACM \u201959 (Western)","author":"La Briandais Rene De","year":"1959","unstructured":"Rene De La Briandais . File searching using variable length keys. In Papers Presented at the the March 3-5, 1959 , Western Joint Computer Conference, IRE-AIEE-ACM \u201959 (Western) , pages 295\u2013 298 , New York, NY, USA , 1959 . ACM. Rene De La Briandais. File searching using variable length keys. In Papers Presented at the the March 3-5, 1959, Western Joint Computer Conference, IRE-AIEE-ACM \u201959 (Western), pages 295\u2013298, New York, NY, USA, 1959. ACM."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9378-0"},{"key":"e_1_3_2_1_4_1","volume-title":"Gallery of Verified Programs","author":"Filli\u00e2tre Jean-Christophe","year":"2015","unstructured":"Jean-Christophe Filli\u00e2tre . Purely applicative heaps implemented with Braun trees . Gallery of Verified Programs , 2015 . http:\/\/toccata.lri.fr\/ gallery\/braun_trees.en.html , Formal proof development. Jean-Christophe Filli\u00e2tre. Purely applicative heaps implemented with Braun trees. Gallery of Verified Programs, 2015. http:\/\/toccata.lri.fr\/ gallery\/braun_trees.en.html , Formal proof development."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/367390.367400"},{"issue":"2","key":"e_1_3_2_1_6_1","first-page":"173","article-title":"Tool support for the interactive derivation of formally correct functional programs","volume":"9","author":"Guttmann Walter","year":"2003","unstructured":"Walter Guttmann , Helmuth Partsch , Wolfram Schulte , and Ton Vullinghs . Tool support for the interactive derivation of formally correct functional programs . Journal of Universal Computer Science , 9 ( 2 ): 173 \u2013 188 , Feb 2003 . Walter Guttmann, Helmuth Partsch, Wolfram Schulte, and Ton Vullinghs. Tool support for the interactive derivation of formally correct functional programs. Journal of Universal Computer Science, 9(2):173\u2013188, Feb 2003.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"207","volume-title":"Mathematics of Program Construction, Second International Conference","author":"Hoogerwoord Rob R.","unstructured":"Rob R. Hoogerwoord . A logarithmic implementation of flexible arrays . In R. Bird, C. Morgan, and J. Woodcock, editors, Mathematics of Program Construction, Second International Conference , volume 669 of LNCS , pages 191\u2013 207 . Springer, 1992. Rob R. Hoogerwoord. A logarithmic implementation of flexible arrays. In R. Bird, C. Morgan, and J. Woodcock, editors, Mathematics of Program Construction, Second International Conference, volume 669 of LNCS, pages 191\u2013207. Springer, 1992."},{"key":"e_1_3_2_1_8_1","volume-title":"Systematic Software Development using VDM","author":"Jones Cliff B.","year":"1990","unstructured":"Cliff B. Jones . Systematic Software Development using VDM . Prentice Hall International , 2 nd edition, 1990 . Cliff B. Jones. Systematic Software Development using VDM. Prentice Hall International, 2nd edition, 1990.","edition":"2"},{"key":"e_1_3_2_1_9_1","volume-title":"Archive of Formal Proofs","author":"Nipkow Tobias","year":"2014","unstructured":"Tobias Nipkow . Priority queues based on Braun trees . Archive of Formal Proofs , 2014 . http:\/\/devel.isa-afp.org\/entries\/Priority_Queue_Braun. html (development) and http:\/\/isa-afp.org\/entries\/Priority_Queue_ Braun.html (latest release), Formal proof development. Tobias Nipkow. Priority queues based on Braun trees. Archive of Formal Proofs, 2014. http:\/\/devel.isa-afp.org\/entries\/Priority_Queue_Braun. html (development) and http:\/\/isa-afp.org\/entries\/Priority_Queue_ Braun.html (latest release), Formal proof development."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71237-6_13"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9459-3"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics with Isabelle\/HOL","author":"Nipkow Tobias","year":"2014","unstructured":"Tobias Nipkow and Gerwin Klein . Concrete Semantics with Isabelle\/HOL . Springer , 2014 . 298 pp. http:\/\/concrete-semantics.org . Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle\/HOL. Springer, 2014. 298 pp. http:\/\/concrete-semantics.org ."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence Paulson and Markus Wenzel . Isabelle\/ HOL \u2014 A Proof Assistant for Higher-Order Logic volume 2283 of LNCS . Springer 2002 . 218 pp. Tobias Nipkow Lawrence Paulson and Markus Wenzel. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic volume 2283 of LNCS. Springer 2002. 218 pp.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002876"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511811326","volume-title":"ML for the Working Programmer","author":"Paulson Lawrence C.","year":"1996","unstructured":"Lawrence C. Paulson . ML for the Working Programmer . Cambridge University Press , 2 nd edition, 1996 . Lawrence C. Paulson. ML for the Working Programmer. Cambridge University Press, 2nd edition, 1996.","edition":"2"},{"key":"e_1_3_2_1_16_1","volume-title":"A logarithmic implementation of flexible arrays. Memorandum MR83\/4","author":"Rem Martin","year":"1983","unstructured":"Martin Rem and Wim Braun . A logarithmic implementation of flexible arrays. Memorandum MR83\/4 . Eindhoven University of Techology , 1983 . Martin Rem and Wim Braun. A logarithmic implementation of flexible arrays. Memorandum MR83\/4. Eindhoven University of Techology, 1983."},{"key":"e_1_3_2_1_17_1","first-page":"32","volume-title":"International Conference on Theorem Proving in Higher Order Logics","author":"Slind Konrad","unstructured":"Konrad Slind and Michael Norrish . A brief overview of HOL4 . In International Conference on Theorem Proving in Higher Order Logics , pages 28\u2013 32 . Springer, 2008. Konrad Slind and Michael Norrish. A brief overview of HOL4. In International Conference on Theorem Proving in Higher Order Logics, pages 28\u201332. Springer, 2008."}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"New Orleans LA USA","acronym":"POPL '20"},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373834","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373834","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:22Z","timestamp":1750202002000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373834"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":17,"alternative-id":["10.1145\/3372885.3373834","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373834","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}