We define a typed assembly language, HBAL, with features for reusing heap space with differing types. A type system with linearity constraints is used to ensure soundness, which we prove against an untyped memory-and-registers machine model.David Aspinall and Adriana Compagnoni.
Click here to return to my papers page.