%T Proofs of Soundness and Strong Normalization for Linear Memory Types
%A Heng Huang
%A Chris Hawblitzel
%R Technical Report TR2002-437
%I Dartmouth College, Computer Science
%C Hanover, NH
%D November 2002
%U http://www.cs.dartmouth.edu/reports/TR2002-437.ps.Z
%X
 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.