A type theory for memory allocation and data layout.

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Browse the full POPL paper archive.