Study on Highly Reliable Programming Languages for Code Generation
| Project/Area Number |
25280020
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Partial Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
ASAI Kenichi お茶の水女子大学, 人間文化創成科学研究科, 准教授 (10262156)
IGARASHI Atsushi 京都大学, 情報学研究科, 教授 (40323456)
UNNO Hiroshi 筑波大学, システム情報系, 助教 (80569575)
|
|---|
| Co-Investigator(Renkei-kenkyūsha) |
KISELYOV Oleg 東北大学, 情報科学研究科, 助教 (50754602)
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥17,290,000 (Direct Cost: ¥13,300,000、Indirect Cost: ¥3,990,000)
Fiscal Year 2015: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
Fiscal Year 2014: ¥4,810,000 (Direct Cost: ¥3,700,000、Indirect Cost: ¥1,110,000)
Fiscal Year 2013: ¥7,670,000 (Direct Cost: ¥5,900,000、Indirect Cost: ¥1,770,000)
|
|---|
| Keywords | ディペンダブルコンピューティング / 関数型プログラム言語 / プログラム生成 / プログラム検証 / プログラム変換 / プログラム特化 / 高性能計算 / 型システム / 関数型プログラミング言語 / 実行時プログラム生成 / プログラミング言語 / ソフトウェア検証 |
|---|
| Outline of Final Research Achievements |
Code generation is a leading approach to generate, for a given generic program, specialized code for individual environments, parameters, and architectures. In this research we have developed theories and programming languages for safe and highly reliable code generation, and have also implemented them. Our major results include: (1) We succeeded in designing and implementing a new type system in which one can use various side effects such as mutation and control operators as well as can write code generators, yet the system ensures well typedness and well scopedness statically. (2) We have designed and implemented a new language for generating efficient database queries in SQL that is type safe. (3) We have proposed an automatic technique for inserting staging annotations to programs that are guaranteed to be optimal. We believe that these results and many others of our research contributed to enhance the safety and reliability of program generation techniques.
|
Report
(4 results)
Research Products
(26 results)
-
-
-
-
-
-
-
[Journal Article] Temporal Verification of Higher-Order Functional Programs2016
Author(s)
Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno
-
Journal Title
In Proceedings of the 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), ACM SIGPLAN Notices
Volume: 51 (1)
Pages: 57-68
DOI
Related Report
Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] コード生成のための自然演繹2014
Author(s)
須藤悠斗、Oleg Kiselyov, 亀山幸義
Organizer
日本ソフトウェア科学会第31回大会
Place of Presentation
名古屋大学（愛知）
Year and Date
2014-09-08 – 2014-09-10
Related Report
-
-
-
-
-
