Data structures such as a doubly linked list and a B+ tree have blocks of memory that have multiple pointers to it. This creates the risk that a bug will allow memory to be accessed after being freed.
I have heard of ideas based around linear typing for guaranteeing memory safety in the case of a single pointer to the memory. I believe the Rust language is based around this.
But suppose, for example, I wanted a memory safe implementation of a B+ tree in a systems language that has no garbage collection or reference counting. What exists in type theory that could be used to guarantee that the B+ tree implementation is memory safe?