Study on Highly Reliable Programming Languages for Code Generation

用于代码生成的高可靠编程语言研究

• 批准号: 25280020
• 负责人: KAMEYAMA YUKIYOSHI
• 金额: $ 11.07万
• 依托单位: University of Tsukuba
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B)
• 财政年份: 2013
• 资助国家: 日本
• 起止时间: 2013-04-01 至 2016-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25280020/
• 关键词: ディペンダブルコンピューティング; 関数型プログラム言語; プログラム生成; プログラム検証; プログラム変換; プログラム特化; 高性能計算; 型システム; 関数型プログラミング言語; 実行時プログラム生成; プログラミング言語; ソフトウェア検証

项目成果

Temporal Verification of Higher-Order Functional Programs

高阶函数程序的时间验证

• DOI: 10.1145/2837614.2837667
• 发表时间: 2016
• 期刊: In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices
• 作者: Akihiro Murase;Tachio Terauchi;Naoki Kobayashi;Ryosuke Sato;and Hiroshi Unno
• 通讯作者: and Hiroshi Unno

A Type Theoretic Specification of Partial Evaluation

部分评估的类型理论规范

• 发表时间: 2014
• 期刊: Proc. of 2014 Symp. on Principles and Practice of Declarative Programming
• 作者: K. Asai;L. Fennell;P. Thiemann;Y. Zhang
• 通讯作者: Y. Zhang

Agda による定式化された型推論器の拡張と改良

Agda 形式化类型推断器的扩展和改进

• 发表时间: 2016
• 期刊: 第１８回プログラミングおよびプログラミング言語ワークショップ予稿集（オンライン）
• 作者: 門脇 香子;浅井 健一
• 通讯作者: 浅井 健一

Combinators for impure yet hygienic code generation

用于生成不纯净但卫生的代码的组合器

• DOI: 10.1016/j.scico.2015.08.007
• 发表时间: 2015
• 期刊: Science of Computer Programming
• 影响因子: 1.3
• 作者: Yukiyoshi Kameyama;Oleg Kiselyov;Chung-chieh Shan
• 通讯作者: Chung-chieh Shan

Formalizing a Correctness Property of a Type-Directed Partial Evaluator

形式化类型导向部分求值器的正确性属性

• DOI: 10.1145/2541568.2541572
• 发表时间: 2014
• 期刊: Proc. of ACM SIGPLAN Workshop on Programming Language meets Program Verification
• 作者: A.K.M. Mahfuzul Islam;Tohru Ishihara;and Hidetoshi Onodera;清水直;Noriko Hirota and Kenichi Asai
• 通讯作者: Noriko Hirota and Kenichi Asai