A dependently typed assembly language
A dependently typed assembly language
复制标题
DOI：
10.1145/507669.507657
复制
发表时间：
2001-10-01
影响因子：
--
通讯作者：
Harper, R
中科院分区：
文献类型：
--
作者：
Xi, HW;Harper, R
我们提出了一个依赖类型的汇编语言（DTAL），其中的类型系统支持使用的依赖类型的限制形式，在汇编级依赖类型的一些好处。DTAL对TAL进行了改进，支持某些重要的编译器优化，如运行时数组边界检查消除和标记检查消除。此外，DTAL正式解决了在汇编级表示和类型的问题，使其不仅适用于处理ML中的数据库，而且适用于处理依赖ML（DML）中的依赖数据库。
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).