Looks like a neat paper anyway. The abstract is:
We explore foundational typing support for strong updates — updating a memory cell to hold values of unrelated types at different points in time. We present a simple, but expressive type system based upon standard linear logic, one that also enjoys a simple semantic interpretation for types that is closely related to models for spatial logics. The typing interpretation is strong enough that, in spite of the fact thato ur core calculus supports shared, mutable references and cyclic graphs, every well-typed program terminates. We then consider extensions needed to make our calculus expressive enough to serve as a model for languages with ML-style references, where the capability to access a reference cell is unrestricted, but strong updates are disallowed. Our extensions include a thaw primitive for temporarily re-gaining the capability to perform strong updates on unrestricted references.
---
Man if someone could scan in a copy of page 168 of Theoretical Computer Science volume 59 ("The Linear Abstract Machine", Yves Lafont, from 1988), I would be super grateful; The Penn library doesn't seem to have a paper copy, and refers me to ScienceDirect, whcih has the article but accidentally included page 193 where 168 should be, and page 168 unfortunately, I believe, contains only the most important definition of the entire paper in Table 1. I think it also has Tables 2 and 3, since alls I see is Tables 4 and onward.
