Towards Highly Universal Typed Intermediate Languages

在这项研究中，我们试图通过追求基于RISC的抽象机来设计高度通用的、快速类型的中间语言。在现有低级指令序列依赖类型类型检查技术的基础上，研究了(1)用于实现位级操作中的固定数和支持移位指令的大小写相关类型和二叉判定图(BDDS)的新概念；(2)用于支持循环数据结构的类型化构造的新概念；(3)用于以结构化方式支持快速多维数组操作的基于下标计算的新谓词。

In this study, we tried to design highly universal and fast typed intermediate languages by pursuing RISC-based abstract machines. On the basis of the existing techniques of type checking with dependent types for low-level instruction sequences, we examined (1) a new notion of case dependent types and binary decision diagrams (BDDs) for implementing fixnums and supporting the shift instructions in bit-level operations, (2) a new notion of provisional assumptions for supporting typed construction of cyclic data structures, and (3) a new predicate on subscript calculation for supporting fast multidimensional array operations in a structural manner.