{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:22:21Z","timestamp":1742952141830,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031562211"},{"type":"electronic","value":"9783031562228"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-56222-8_14","type":"book-chapter","created":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T08:02:30Z","timestamp":1710835350000},"page":"243-254","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Region Quadtrees Verified"],"prefix":"10.1007","author":[{"given":"Tobias","family":"Nipkow","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"14_CR1","unstructured":"Agda. https:\/\/github.com\/agda\/agda"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Aluru, S.: Quadtrees and octrees. In: Mehta, D.P., Sahni, S. (eds.) Handbook of Data Structures and Applications, 2nd edn. Chapman and Hall\/CRC, Boca Raton (2017). https:\/\/doi.org\/10.1201\/9781315119335","DOI":"10.1201\/9781315119335"},{"key":"14_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"14_CR4","unstructured":"Brouwer, J.: Practical verification of quadtrees (2021). http:\/\/resolver.tudelft.nl\/uuid:550c654e-0443-4f00-bab3-d24ed3afc879"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_31"},{"issue":"3","key":"14_CR6","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1232420.1232424","volume":"29","author":"JN Foster","year":"2007","unstructured":"Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29(3), 17 (2007). https:\/\/doi.org\/10.1145\/1232420.1232424","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR7","unstructured":"Nipkow, T.: Region quadtrees. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/Region_Quadtrees.html. Formal proof development"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics with Isabelle\/HOL. Springer, Heidelberg (2014). http:\/\/concrete-semantics.org","DOI":"10.1007\/978-3-319-10542-0"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"14_CR10","unstructured":"Rau, M.: Multidimensional binary search trees. Archive of Formal Proofs (2019). https:\/\/isa-afp.org\/entries\/KD_Tree.html. Formal proof development"},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1145\/356924.356930","volume":"16","author":"H Samet","year":"1984","unstructured":"Samet, H.: The quadtree and related hierarchical data structures. ACM Comput. Surv. 16(2), 187\u2013260 (1984). https:\/\/doi.org\/10.1145\/356924.356930","journal-title":"ACM Comput. Surv."},{"key":"14_CR12","volume-title":"The Design and Analysis of Spatial Data Structures","author":"H Samet","year":"1990","unstructured":"Samet, H.: The Design and Analysis of Spatial Data Structures. Addison-Wesley, Boston (1990)"},{"issue":"4","key":"14_CR13","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/0020-0190(85)90049-3","volume":"20","author":"DS Wise","year":"1985","unstructured":"Wise, D.S.: Representing matrices as quadtrees for parallel processors. Inf. Process. Lett. 20(4), 195\u2013199 (1985). https:\/\/doi.org\/10.1016\/0020-0190(85)90049-3","journal-title":"Inf. Process. Lett."},{"key":"14_CR14","unstructured":"Wise, D.S.: Parallel decomposition of matrix inversion using quadtrees. In: International Conference on Parallel Processing, ICPP 1986, pp. 92\u201399. IEEE Computer Society Press (1986)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-18317-5_9","volume-title":"Functional Programming Languages and Computer Architecture","author":"DS Wise","year":"1987","unstructured":"Wise, D.S.: Matrix algebra and applicative programming. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 134\u2013153. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-18317-5_9"},{"key":"14_CR16","unstructured":"Wise, D.S.: Matrix algorithms using quadtrees (invited talk). In: Hains, G., Mullin, L.M.R. (eds.) ATABLE-92, International Workshop on Arrays, Functional Languages and Parallel Systems (1992). https:\/\/legacy.cs.indiana.edu\/ftp\/techreports\/TR357.pdf"}],"container-title":["Lecture Notes in Computer Science","Taming the Infinities of Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-56222-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T22:03:32Z","timestamp":1730930612000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-56222-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031562211","9783031562228"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-56222-8_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"20 March 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}