BIB-VERSION:: CS-TR-v2.0
ID:: ncstrl.dartmouthcs//TR2003-468
ENTRY:: August 09, 2003
ORGANIZATION:: Dartmouth College, Computer Science
TITLE:: Formal Properties of Linear Memory Types
TYPE:: Technical Report (paper)
REVISION:: 1
AUTHOR:: Huang, Heng
AUTHOR:: Wittie, Lea
AUTHOR:: Hawblitzel, Chris
DATE:: August 2003
RETRIEVAL:: For a paper copy, email <reports@cs.dartmouth.edu>
RETRIEVAL:: For a paper copy, write to
       Technical Report Librarian
       Department of Computer Science
       Dartmouth College
       6211 Sudikoff Laboratory
       Hanover, NH 03755-3510
       USA
RETRIEVAL:: Compressed Postscript at http://www.cs.dartmouth.edu/reports/TR2003-468.ps.Z
RETRIEVAL:: PDF at http://www.cs.dartmouth.edu/reports/TR2003-468.pdf
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.
END:: ncstrl.dartmouthcs//TR2003-468