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
Published in:ACM SIGPLAN Notices
Main Authors: Xi, Hongwei, Harper, Robert
Format: Article in Journal/Newspaper
Language:English
Published: Association for Computing Machinery (ACM) 2001
Subjects:
DML
Online Access:http://dx.doi.org/10.1145/507669.507657
https://dl.acm.org/doi/pdf/10.1145/507669.507657
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