We present a dependently typed assembly language (DTAL) in which the
type system supports the use of a restricted form of dependent types,
reaping some benefits of dependent types at assembly level. DTAL
improves upon TAL, enabling certain important compiler optimizations
such as run-time array bound check elimination and tag check elimination.
Also, DTAL formally addresses the issue of representing sum types at
assembly level, making it suitable to handle not only datatypes in ML
but also dependent datatypes in Dependent ML (DML).
