L3: A Linear Language with Locations

8 years 12 months ago
L3: A Linear Language with Locations
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 that our 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.
Greg Morrisett, Amal J. Ahmed, Matthew Fluet
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors Greg Morrisett, Amal J. Ahmed, Matthew Fluet
Comments (0)