{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:02:27Z","timestamp":1767927747777,"version":"3.49.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T00:00:00Z","timestamp":1673481600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T00:00:00Z","timestamp":1673481600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1007\/s10817-022-09655-x","type":"journal-article","created":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T06:02:56Z","timestamp":1673503376000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Efficient Extensional Binary Tries"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8971-9171","authenticated-orcid":false,"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,12]]},"reference":[{"key":"9655_CR1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:4)2011","author":"A Abel","year":"2011","unstructured":"Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Log. Methods Comput. Sci. (2011). https:\/\/doi.org\/10.2168\/LMCS-7(2:4)2011","journal-title":"Log. Methods Comput. Sci."},{"key":"9655_CR2","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Verified Software Toolchain. In: 20th European Symposium on Programming (ESOP\u201911), LNCS, vol. 6602, 1\u201317. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"9655_CR3","unstructured":"Appel, A.W.: Verified Functional Algorithms, Software Foundations, vol.\u00a03. softwarefoundations.org (2017). https:\/\/softwarefoundations.cis.upenn.edu\/vfa-current"},{"key":"9655_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program logics for certified compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program logics for certified compilers. Cambridge University Press, Cambridge (2014)"},{"key":"9655_CR5","doi-asserted-by":"publisher","unstructured":"Beringer, L.: Verified software units. In: 30th European Symposium on Programming (ESOP\u201921), LNCS, vol. 12648, 118\u2013147. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_5","DOI":"10.1007\/978-3-030-72019-3_5"},{"issue":"1","key":"9655_CR6","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/s10703-020-00353-1","volume":"58","author":"L Beringer","year":"2021","unstructured":"Beringer, L., Appel, A.W.: Abstraction and subsumption in modular verification of C programs. Formal Methods Syst. Des. 58(1), 322\u2013345 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00353-1","journal-title":"Formal Methods Syst. Des."},{"key":"9655_CR7","doi-asserted-by":"publisher","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2. In: Practical Aspects of Declarative Languages, 4th International Symposium (PADL\u201902), LNCS, vol. 2257, pp. 9\u201327. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45587-6_3","DOI":"10.1007\/3-540-45587-6_3"},{"issue":"1\u20134","key":"9655_CR8","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1\u20134), 367\u2013422 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9457-5","journal-title":"J. Autom. Reason."},{"key":"9655_CR9","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., Letouzey, P.: Functors for proofs and programs. In: 13th European Symposium on Programming, ESOP 2004, LNCS, vol. 2986, pp. 370\u2013384. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_26","DOI":"10.1007\/978-3-540-24725-8_26"},{"key":"9655_CR10","doi-asserted-by":"crossref","unstructured":"Gordon, M.J., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science, vol. 78. Springer, New York (1979)","DOI":"10.1007\/3-540-09724-4"},{"key":"9655_CR11","doi-asserted-by":"publisher","unstructured":"Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL 2015: 42nd symposium Principles of Programming Languages, pp. 247\u2013259. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676966","DOI":"10.1145\/2676726.2676966"},{"key":"9655_CR12","unstructured":"Krebbers, R., et\u00a0al.: The Coq-std++ extended standard library, module stdpp.pmap (2012\u20132021). https:\/\/plv.mpi-sws.org\/coqdoc\/stdpp\/stdpp.pmap.html"},{"issue":"7","key":"9655_CR13","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"9655_CR14","unstructured":"Leroy, X., Appel, A.W.: Canonical binary trees, the Coq development, version 2 (2022). https:\/\/github.com\/xavierleroy\/canonical-binary-tries\/tree\/v2. Software Heritage ID swh:1:dir:02996583ae02411d8e1e7c3f20bc12b0eebbf96a"},{"key":"9655_CR15","unstructured":"Leroy, X., Appel, A.W., Doligez, D.: The CompCert verified C compiler, module Maps (2021\u20132022). https:\/\/compcert.org\/doc-3.10\/html\/compcert.lib.Maps.html. Software Heritage ID swh:1:cnt:0d83aa98a1d7cc150a3164ad487d9cde9c00a64f"},{"key":"9655_CR16","unstructured":"Leroy, X., Doligez, D.: The CompCert verified C compiler, module Maps (2005\u20132021). https:\/\/compcert.org\/doc-3.9\/html\/compcert.lib.Maps.html. Software Heritage ID swh:1:cnt:6bc6e14bf54f778029e13b192aaab53dd5e819a4"},{"key":"9655_CR17","unstructured":"Letouzey, P.: MMaps: Modular finite maps over ordered types (2015\u20132020). https:\/\/github.com\/letouzey\/coq-mmaps"},{"key":"9655_CR18","unstructured":"Nipkow, T., Blanchette, J., Eberl, M., G\u00f3mez-Londo\u00f1o, A., Lammich, P., Sternagel, C., Wimmer, S., Zhan, B.: Functional Algorithms, Verified! (2021). https:\/\/functional-algorithms-verified.org"},{"key":"9655_CR19","doi-asserted-by":"publisher","DOI":"10.1145\/3498693","author":"L Pujet","year":"2022","unstructured":"Pujet, L., Tabareau, N.: Observational equality: now for good. Proc. ACM Program. Lang. (2022). https:\/\/doi.org\/10.1145\/3498693","journal-title":"Proc. ACM Program. Lang."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09655-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09655-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09655-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,24]],"date-time":"2023-03-24T09:23:08Z","timestamp":1679649788000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09655-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,12]]},"references-count":19,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["9655"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09655-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,12]]},"assertion":[{"value":"10 October 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 October 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 January 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"There are no conflicts of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"Code is available at .","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Code availability"}}],"article-number":"8"}}