Towards Highly Universal Typed Intermediate Languages

迈向高度通用的类型中间语言

• 批准号: 23650013
• 负责人: YASUGI Masahiro
• 金额: $ 2.25万
• 依托单位: Kyushu Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Challenging Exploratory Research
• 财政年份: 2011
• 资助国家: 日本
• 起止时间: 2011 至 2013
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23650013/
• 关键词: 型付中間言語; 低水準言語; プログラミング言語処理系; 型検査; 多次元配列; 循環データ構造; 高性能計算; 計算機システム; プログラミング言語; ソフトウエア開発効率化・安定化; ディペンダブル・コンピューティング; ハイパフォーマンス・コンピューティング

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.

在本研究中，我们试图通过追求基于 RISC 的抽象机来设计高度通用和快速类型的中间语言。 基于低级指令序列的依赖类型的现有类型检查技术，我们研究了（1）案例依赖类型和二进制决策图（BDD）的新概念，用于实现固定数并支持位移位指令级别操作，（2）用于支持循环数据结构的类型化构造的临时假设的新概念，以及（3）用于以结构方式支持快速多维数组操作的下标计算的新谓词。

项目成果

ビットレベル低水準命令列のBDDに基づく検証技法に関する考察

基于BDD的位级低级指令序列验证技术的思考

• 发表时间: 2011
• 作者: 八杉 昌宏

ビットレベル低水準命令列のBDDに基づく検証技法に関する考察

基于BDD的位级低级指令序列验证技术的思考

• 发表时间: 2011
• 作者: 八杉昌宏

Typed Construction of Cyclic Data Structures Using Provisional Assumptions

使用临时假设的循环数据结构的类型化构造

• 发表时间: 2012
• 作者: Masahiro Yasugi

Typed Construction of Cyclic Data Structures Using Provisional Assumptions

使用临时假设的循环数据结构的类型化构造

• 作者: Masahiro Yasugi

高速な多次元配列操作のための型検査方式の検討

高速多维数组运算类型检查方法研究

• 发表时间: 2013
• 作者: 八杉昌宏