Heap Bounded Assembly Language (HBAL)



This project studies a first-order linerly typed assembly language, HBAL, thaa allows the safe reuse of heap space for elements of different types. Linerly typing ensures the single pointer property, disallowing aliasing, but allowing safe in-place upddate compilation of programming languages.

Our ultimate goal is to design a family of assembly languages which have high-level typing features wich are used to expresss resource bound constraints. We want to link up the assmbly 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 (Hoffmann 2000). 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.

Participants: David Aspinall, Adriana Compagnoni, Ricardo Medel, Eduardo Bonelli, and Matthieu Lucotte.
Test the LFPL Compiler
Test the HBAL Typechecker
Test the HBAL Machine Model

This material is based upon work supported by the National Science Foundation under Grant No. 0093362, and the New Jersey Commission on Science and Technology.

Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation or the New Jersey Commission on Science and Technology.