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 overcomes several
significant limitations in recently proposed low-level languages including
Java bytecode language and a typed assembly language, which prevent them from
handling certain important compiler optimizations such as run-time array bound
check elimination. We also mention a compiler which can generate DTAL code
from compiling some high-level programs.