%T Formal Properties of Linear Memory Types
%A Heng Huang
%A Lea Wittie
%A Chris Hawblitzel
%R Technical Report TR2003-468
%I Dartmouth College, Computer Science
%C Hanover, NH
%D August 2003
%U http://www.cs.dartmouth.edu/reports/TR2003-468.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 of preservation, progress, strong normalization, erasure, and translation correctness.