Towards Highly Universal Typed Intermediate Languages

在这项研究中，我们试图通过追求基于risc的抽象机器来设计高度通用和快速类型的中间语言。在现有的低级指令序列依赖类型类型检查技术的基础上，我们研究了(1)用于实现固定和支持位级操作中移位指令的case依赖类型和二进制决策图（bdd）的新概念；(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.