Type theory for memory safe data structures
There has been a lot of work around the idea of statically checking the memory safety properties of programs.

Francois Pottier give an excellent overview of various approaches in this presentation. The main technique you probably would be interested in is region typing.

The Wikipedia article is quite complete, but the basic idea is to keep explicit regions which references are required to explicitly be assigned to a given region, which can be managed by the programmer or left to be inferred by the compiler. This is somewhat reminiscent of the RAII approach to memory management used mainly in C++ (the wiki article is terrible however).

In practice, region inference hasn't gained widespread use in compilers, mainly because of the complexity of the analyses involved.

Again related, there has been a flurry in work on separation logic over the last decade, which is an extension of Hoare Logic which allows reasoning over separate regions of the heap, in order to analyze whether objects can share memory locations or not. This method of reasoning is quite difficult to apply to a language like C with "real" pointers, because of the possibility of pointer aliasing.