@TechReport{Dartmouth:TR2002-437,
  author = {Heng Huang and Chris Hawblitzel},
  title = {{Proofs of Soundness and Strong Normalization for Linear Memory Types}},
  institution = {Dartmouth College, Computer Science},
  address = {Hanover, NH},
  number = {TR2002-437},
  year = {2002},
  month = {November},
  URL = {http://www.cs.dartmouth.edu/reports/TR2002-437.ps.Z},
  abstract = {
    Efficient low-level systems need more control over memory than safe high-level languages usually provide. As a result, run-time systems are typically written in unsafe languages such as C. This report describes an abstract machine designed to give type-safe code more control over memory. It includes complete definitions and proofs.
  }
}