Linear/affine lifetimes without subtyping
Linear and affine typing systems have been developed in the context of linear logic and process calculi. Most developments of such types do not use subtyping. The system in (1) is pioneering for its use of linearity, as are (2, 3) which introduced session types which are heavily based on linearity. See also the CSTheory Stackexchange thread Determinism and pi-calculus for some other (related) typing systems that make heavy use of linearity and affinity. While all this work is for process calculi, note that sequential behaviour is a well-behaved special case of concurrency and affinity in Rust is closely related (the same) as affinity in process theory.



 N. Kobayashi, B. C. Pierce, D. N. Turner, Linearity and the Pi-Calculus.

 K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.

 K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.