Title: A Formal Semantics For Weak References

Abstract:
  Generally speaking, a weak reference is a reference to an object
that is not followed by the garbage collector.  That is, a weak
reference is not capable of keeping the object it references from
being garbage collected.  Weak references remain a notorious
programming feature largely because there is not an accepted, precise
semantics that describes their behavior (in fact, there have been few
attempts to define their semantics at all).  The trouble seems to be
that weak references allow reachable objects to be garbage collected,
therefore allowing garbage collection to influence the result of a
program.  Despite this setback, weak references continue to be used in
practise and are included in many popular programming languages such
as Standard ML, Haskell, OCaml, and Java.

  We give a formal semantics for a calculus called lambda_weak that
includes weak references and is derived from Morrisett, Harper, and
Felleisen's lambda_gc.  We also discuss methods in which we can
recover unique results from the evaluation of our programs.  After
defining conditions that allow other garbage collection algorithms to
co-exists with our semantics of weak references, we introduce a type
systems and a corresponding type inference algorithm.  We prove the
type system sound and the inference algorithm sound and complete with
respect to the type system.