| Project/Area Number |
20H00582
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (A)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Review Section |
Medium-sized Section 60:Information science, computer engineering, and related fields
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
池渕 未来 京都大学, 情報学研究科, 助教 (70961796)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 准教授 (80828476)
田邉 裕大 東京工業大学, 情報理工学院, 助教 (30985198)
松下 祐介 京都大学, 情報学研究科, 特別研究員(PD) (41003875)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥44,460,000 (Direct Cost: ¥34,200,000、Indirect Cost: ¥10,260,000)
Fiscal Year 2024: ¥8,450,000 (Direct Cost: ¥6,500,000、Indirect Cost: ¥1,950,000)
Fiscal Year 2023: ¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2022: ¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2021: ¥8,840,000 (Direct Cost: ¥6,800,000、Indirect Cost: ¥2,040,000)
Fiscal Year 2020: ¥9,490,000 (Direct Cost: ¥7,300,000、Indirect Cost: ¥2,190,000)
|
|---|
| Keywords | プログラミング言語 / プログラム検証 / 相互運用性 / ソフトウェア契約 / ソフトウエア契約 |
|---|
| Outline of Research at the Start |
近年のソフトウェアシステムは、プログラミング言語に対して言語間相互運用性を要請することが多くなっている。しかし、言語間相互運用性を活用しつつ、正しく動くソフトウェアを構築するのは、単一の言語でのソフトウェア開発よりもさらに困難である。我々は「言語間相互運用を活用したソフトウェアシステムを正しく構築するための技術はどうあるべきか」を研究課題の核心をなす学術的「問い」として据え、ソフトウェア契約というソフトウェア検証のための方法論を、言語間相互運用性とシステムの高信頼性を確保するための技術として拡張・発展させる研究を行う。
|
| Outline of Annual Research Achievements |
【研究項目1. モジュール間のデータ変換機構とその自動化の研究】について、レコードとハッシュテーブル間の相互運用だけでなく、いくつかのデータ型の組み合わせについて一般化を試みたが、その方向ではあまりよい成果が得られなかった。一方、関連した結果として、多段階計算と呼ばれるプログラムコードをデータとして扱えるプログラミング言語について、段階を跨った型抽象のためのモジュールシステム機構を提唱し、その理論の形式化をした論文をFLOPS2024で発表した。
【研究項目2. 多言語モジュールで構成されたソフトウェアシステムの検証機構】(項目2-2)では、多相型を持つ言語と動的型付言語間の相互運用を行うための実行検査について、一部の場面でパラメトリシティ性を諦めれば可能である、ということを計算体系として形式化し理論の正当性証明を行った。この結果は ACM SIGPLAN PLDI 2024 で発表した。ここまでで理論的な結果が整備されてきたため、漸進的型付け言語のコンパイル手法の研究を行い、PPL2025でポスター発表を行った。
(項目2-1)の「データ変換を行う仕組みと実行時検査機構を組み合わせる手法の検討」については前年度に引き続き関連研究のサーベイなどを進めた。また、Rust言語とLinear Haskell言語の相互運用性についての研究を行い、PPL2025でポスターの発表をした(ポスター賞受賞)。
また、ソフトウェア検証技術についても、ACM SIGPLAN ICFP, APLAS, JFP などで論文発表を行った。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
項目2-2については、ACMのトップカンファレンスで発表するなど大きな成果が出ている。その他の課題も当初目論んでいた成果以外の関連する成果が、多段階計算のモジュール化機構やRustとLinear Haskellの相互運用性の研究を含め多数出てきており、「おおむね順調」といえる。
|
| Strategy for Future Research Activity |
研究項目1のデータ変換方式の一般化についてはあまり目処が立っておらず、ふたたび具体的な組み合わせを検討していくよう方針の変更を検討している。RustとLinear Haskellの相互運用性研究や漸進的型付け言語のコンパイラ実装については、新たな研究分担者2名(このうち1名は、本課題でのポスドクであった)を得て加速が見込める。
|
