I’m wondering what academic work (if any?) gave rise to the concept of lifetimes. The FAQ mentions such work, but just points to the bibliography, and none of the listed papers seem like an obvious source for that work. The closest is a paper on Cyclone. Is that the only or best available reference? Or is there some other language that might help?
There is “Effect Types and Region-Based Memory Management” chapter in the advanced tapl. I think it will include some pointers, but I haven’t read it yet.
The above references are good for some of Rust’s lifetime influences. I also think the following is an unacknowledged landmark in terms of applications of linear type systems in programming languages, which Rust has exploited quite effectively:
and similarly, for some interesting, recent formal treatments for reasoning about the heap, there is separation logic, a good paper here: