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