Reference counting as a computational interpretation of linear logic

Jawahar Chirimar, Carl A. Gunter and Jon G. Riecke

We develop an operational model for a language based on linear logic. Our semantics is ‘low-level’ enough to express sharing and copying while still being ‘high-level’ enough to abstract away from details of memory layout, and thus can be used to test potential applications of linear logic for analysis of programs. In particular, we demonstrate a precise relationship between type correctness for the linear-logic-based language and the correctness of a reference-counting interpretation of the primitives, and formulate and prove a result describing the possible run-time reference counts of values of linear type.

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/reference-counting-as-a-computational-interpretation-of-linear-logic/57AE85B618932EE0D716556774E73904