A Dependently Typed Assembly Language

14 years 5 months ago
A Dependently Typed Assembly Language
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 the 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 for handling not only datatypes in ML but also dependent datatypes in Dependent ML (DML).
Hongwei Xi, Robert Harper
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2001
Where ICFP
Authors Hongwei Xi, Robert Harper
Comments (0)