A Dependently Typed Assembly Language

Hongwei Xi and Robert Harper

To appear at International Conference on Functional Programming (ICFP01), Firenze, Italy, 3-5 September 2001


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).

Server START Conference Manager
Update Time 11 May 2001 at 15:31:50
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems