<p>There has been a lot of work around the idea of statically checking the memory safety properties of programs.</p>

<p>Francois Pottier give an excellent overview of various approaches in <a href="http://gallium.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf" rel="noreferrer">this presentation</a>. The main technique you probably would be interested in is <a href="http://en.wikipedia.org/wiki/Region-based_memory_management#Region_inference" rel="noreferrer">region typing</a>.</p>

<p>The Wikipedia article is quite complete, but the basic idea is to keep explicit <em>regions</em> which references are required to explicitly be assigned to a given <em>region</em>, which can be managed by the programmer or left to be inferred by the compiler. This is somewhat reminiscent of the <a href="http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization" rel="noreferrer">RAII</a> approach to memory management used mainly in C++ (the wiki article is terrible however).</p>

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

<p>Again related, there has been a flurry in work on <a href="http://en.wikipedia.org/wiki/Separation_logic" rel="noreferrer">separation logic</a> 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 <a href="http://en.wikipedia.org/wiki/Pointer_aliasing" rel="noreferrer">pointer aliasing</a>.</p>

CC BY-SA 3.0
2014-07-26T17:07:03.893Z
2014-07-27T16:59:06.277Z
2014-07-27T16:59:06.277Z
cody
<p>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.</p>

<p>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.</p>

<p>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?</p>

CC BY-SA 3.0
2014-07-23T23:02:43.587Z
Are you familiar with separation logic?
D.W.
<pl.programming-languages><type-theory><linear-logic>
Type theory for memory safe data structures
user782220
# Type theory for memory safe data structures

(Asked by: username_0 on 2014-07-23)

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?

**Tags:** pl.programming-languages, type-theory, linear-logic
> **Comments:**
> **username_1**: Are you familiar with separation logic?  

---

## 1 answers

### Answer by username_2 on 2014-07-26. Score: 6 | Accepted answer

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](http://gallium.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf). The main technique you probably would be interested in is [region typing](http://en.wikipedia.org/wiki/Region-based_memory_management#Region_inference).

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](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) 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](http://en.wikipedia.org/wiki/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](http://en.wikipedia.org/wiki/Pointer_aliasing).


---

