Proofs of Soundness and Strong Normalization for Linear Memory Types

Dartmouth Technical Report TR2002-437

	Heng Huang
	Chris Hawblitzel

Date: November 2002

URL (compressed postscript): <http://www.cs.dartmouth.edu/reports/TR2002-437.ps.Z> (280KB)

URL (PDF): <http://www.cs.dartmouth.edu/reports/TR2002-437.pdf> (276KB)

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.