Abstract: “We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property, disallowing aliasing, but allowing safe in-place update compilation of programming languages. We prove that HBAL is sound for a low-level untyped model of the machine, using a satisfiability relation which captures when a location correctly models a value of some type. This interpretation is closer to the machine than previous abstract machines used for typed assembly language models, and we separate typing of the store from an untyped operational semantics of programs, as would be required for proof-carrying code.

Our ultimate aim is to design a family of assembly languages which have highlevel typing features which are used to express resource bound constraints. We want to link up the assembly level with high-level languages expressing similar constraints, to provide end-to-end guarantees, and a viable framework for proof-carrying code. HBAL is a first exemplifying step in this direction. It is designed as a target low level language for Hofmann’s LFPL (Hofmann, 2000b) language. Programs written in LFPL run in a bounded amount of heap space, and this property carries over when they are compiled to HBAL: the resulting program does not allocate store or assume an external garbage collector. Following LFPL, we include a special diamond resource type which stands for a unit of heap space of uncommitted type, similar in spirit to Tofte-Talpin’s notion of region.”