Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Heap Bounded Assembly Language
Authors: David Aspinall ; Adriana Compagnoni
Date:Sep 2003
Publication Title:Journal of Automated Reasoning (Special Issue on Proof-Carrying Code)
Publication Type:Journal Article Publication Status:Published
Volume No:31(3-4) Page Nos:261-302
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 that 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 that have high-level typing features for expressing resource-bound constraints. We want to link 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 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 that stands for a unit of heap space of uncommitted type.
Links To Paper
(Author's pre-final version)
Bibtex format
author = { David Aspinall and Adriana Compagnoni },
title = {Heap Bounded Assembly Language},
journal = {Journal of Automated Reasoning (Special Issue on Proof-Carrying Code)},
publisher = {Springer},
year = 2003,
month = {Sep},
volume = {31(3-4)},
pages = {261-302},
doi = {10.1023/B:JARS.0000021014.79255.33},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh