Region Quadtrees Verified
摘要
This paper presents the formalization and verification (in the proof assistant Isabelle) of two variants of quadtrees: standard region quadtrees and quadtrees for matrix algebra.