I’m not quite sure whether this belongs in this forum, but I think it does, as it goes beyond what most users want from Rust.

I am a computing science student and I am writing a thesis about the memory safety aspects of Rust. That means I’m interested in the lifetime system, the idea of ownership, etc. My goal is to define formal semantics for a very small subset of Rust, which includes lifetimes. I do understand the notion of lifetimes and I read several books, tutorials and the like (like the Rust book), but none specify how lifetimes work precisely. I hope to figure out what kind of mathematical structure lifetimes most closely resemble. For example, you need to compare lifetimes to tell one is longer than the other, which says something about the mathematical structure lifetimes have to have. I tried looking at the github documentation, but I have a lot of trouble navigating through it to find the (for me) relevent parts. So basically my question is; is there anyone here that can point me in the right direction? For example the right piece of documentation in the github, where I can read more about how exactly lifetimes are implemented? My hope is that I can derive from that what kind of structure I can use for the rest of my thesis.