Proving memory management invariants for a language based on linear logic
Jawahar Chirimar, Carl A. Gunter, Jon G. Riecke · 1992
We develop tools for the rigorous formulation and proof of properties of runtime management for a sample programming language based on a linear type system. Two semantics are diescribed, one at a level of observable results of computations and one describing linear connectives in terms of memory-management primitives. The two semantics are proven equivalent and the memory-management model is proven to satisfy fundamental correctness criteria for reference counts.