L3: A Linear Language with Locations
-
tlca05.pdf
(with Greg Morrisett and Amal Ahmed; Appeared at TLCA'05)
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.
-
techrpt.pdf
(with Amal Ahmed and Greg Morrisett; Harvard University Technical Report;
TR-24-04)
We present a simple, but expressive type system that supports
strong updates -- updating a memory cell to hold values of
unrelated types at different points in time. Our formulation is based
upon standard linear logic and, as a result, 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 model 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 re-gaining the capability to perform strong updates on
unrestricted references. The thaw primitive is closely
related to other mechanisms that support strong updates, such as
Cqual's restrict.
-
popl05.pdf
(with Greg Morrisett and Amal Ahmed; Rejected by POPL'05)
We present a simple, but expressive type system that supports
strong updates -- udating a memory cell to hold values of
unrelated types at different points in time. Our formulation is based
upon standard linear logic and, as a result, 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 model 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 re-gaining the capability to perform strong updates on
unrestricted references. The thaw primitive is closely
related to other mechanisms that support strong updates, such as
Cqual’s restrict,
|
The documents contained in these directories are included by the
contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a non-commercial basis. Copyright and
all rights therein are maintained by the authors or by other copyright
holders, notwithstanding that they have offered their works here
electronically. It is understood that all persons copying this
information will adhere to the terms and constraints invoked by each
author's copyright. These works may not be reposted without the
explicit permission of the copyright holder.
|
|