Formal Properties of Linear Memory Types

Dartmouth Technical Report TR2003-468

	Heng Huang
	Lea Wittie
	Chris Hawblitzel

Date: August 2003

URL (compressed postscript): <http://www.cs.dartmouth.edu/reports/TR2003-468.ps.Z> (448KB)

URL (PDF): <http://www.cs.dartmouth.edu/reports/TR2003-468.pdf> (628KB)

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 of preservation, progress, strong normalization, erasure, and translation correctness.