Heap Bounded Assembly Language

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.
Heap Bounded Assembly Language.
Journal of Automated Reasoning (Special Issue on Proof-Carrying Code), Volume 31, Issue 3-4, Sep 2003, pp 261-302.
Download as ps or pdf (pre-final version).

Click here to return to my papers page.

my Vcard
David R. Aspinall, email david.aspinall@ed.ac.uk.
Contact GPG key (Instant HOWTO)