Semantics of memory safety and borrowing in functional programming languages

Programming languages provide various mechanisms for memory management.

In languages with manual memory management such as C, the programmer must annotate their code with function calls that allocate and deallocate memory where needed.

Other languages such as Java and Haskell have automatic memory management; in this paradigm, the choice of when to deallocate memory is handled at runtime, and so allocations are dynamically disposed of when necessary.

Recently, languages such as Rust have explored a third option, in which allocations of memory are owned by a single object, and are deallocated when the owner falls out of scope.

Such a resource may be loaned to multiple other objects, under the conditions that the loan is rescinded before the owner is destroyed, and that the object in question is not mutated during the loan; we say that the object is borrowed while the loan is active.

In this proposal, I consider several ways that borrowing can be integrated into various type theories, discuss current literature, and propose new avenues of research. (An extended research proposal is attached as a supporting document.)