@inproceedings{086ff9d0e0484c73ae6b449bdfb544bc,
title = "Proving memory management invariants for a language based on linear logic",
abstract = "We develop tools for the rigorous formulation and proof of properties of runtime memory management for a sample programming language based on a linear type system. Two semantics are described, 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.",
author = "Jawahar Chirimar and Gunter, {Carl A.} and Riecke, {Jon G.}",
year = "1992",
doi = "10.1145/141478.141527",
language = "English (US)",
isbn = "0897914813",
series = "Proc 92 ACM Conf Lisp Funct Program",
publisher = "Publ by ACM",
pages = "139--150",
booktitle = "Proc 92 ACM Conf Lisp Funct Program",
note = "Proceedings of the 1992 ACM Conference on Lisp and Functional Programming ; Conference date: 22-06-1992 Through 24-06-1992",
}