A Dependently Typed Assembly Language (Extended Abstract)

) Hongwei Xi Oregon Graduate Institute hongwei@cse.ogi.edu Robert Harper Carnegie Mellon University rwh@cs.cmu.edu Abstract 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 generates code in DTAL from compiling some high-level programs. 1 Introduction A certifying compiler is one that generates object code that can be readily checked for compliance with a specified safety policy that constrains its run-time behavior. By ensuring that compliance is checkable, the code recipient need not be concerned with the origin of the code, only..