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

Full description

Bibliographic Details
Main Authors: Hongwei Xi, Robert Harper
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published: ACM Press 1999
Subjects:
DML
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.1905
http://www.ececs.uc.edu/~hwxi/academic/papers/icfp01.ps
Description
Summary: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).

Similar Items