[bitc-dev] A Garbage-Collecting Typed Assembly Language

[Sandro Magi]

Abstract

Typed assembly languages usually support heap allocation safely,
but often rely on an external garbage collector to deallocate objects
from the heap and prevent unsafe dangling pointers. Even if the
external garbage collector is provably correct, verifying the safety
of the interaction between TAL programs and garbage collection is
nontrivial. This paper introduces a typed assembly language whose
type system is expressive enough to type-check a Cheney-queue
copying garbage collector, so that ordinary programs and garbage
collection can co-exist and interact inside a single typed language.
The only built-in types for memory are linear types describing
individual memory words, so that TAL programmers can define
their own object layouts, method table layouts, heap layouts, and
memory management techniques.

ftp://ftp.research.microsoft.com/pub/tr/TR-2006-169.pdf

Seems relevant to BitC.

Sandro