|
Abstract : |
We develop formal methods for reasoning about memory usage at a level of abstraction suitable for establishing or refuting claims about the potential applications of linear logic for static analysis. In particular, we demonstrate a precise relationship between type correctness for a language based on linear logic and the correctness of a reference-counting interpretation of the primitives that the language draws from the rules for the `of course ' operation. Our semantics is `low-level ' enough to express sharing and copying while still being `highlevel ' enough to abstract away from details of memory layout. This enables the formulation and proof of a result describing the possible run-time reference, |
