The pioneering work of Necula and Lee on Proof- Carrying Code motivated recent developments in typed intermediate languages and typed assembly languages that enforce various security policies during code execution. . In this talk we present ongoing joint work with David Aspinall on the development of a typed assembly language for safe memory space reuse, to be used in a Proof Carrying Code environment. . We present a typed assembly language, HBAL, which has a type system with features for managing space usage. In contrast to other typed assembly languages, HBAL allows memory areas to be reused for values of differing types. We ensure type safety by using a type system with linearity constraints to prevent aliasing of heap locations, together with special pseudo- instructions for altering types at isolated points in the code. The reuse discipline is controlled by compilation from a high-level language, and we demonstrate a compilation from a prototypical first-order functional language, LFPL, due to Hofmann.