2020 Fiscal Year Annual Research Report
Research on software contracts for highly interoperable software modules
| Project/Area Number |
20H00582
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
末永 幸平 京都大学, 情報学研究科, 准教授 (70633692)
関山 太朗 国立情報学研究所, アーキテクチャ科学研究系, 助教 (80828476)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | プログラミング言語 / プログラム検証 / 相互運用性 / ソフトウェア契約 |
|---|
| Outline of Annual Research Achievements |
【研究項目1. モジュール間のデータ変換機構とその自動化の研究】として、レコードとハッシュテーブルの安全な相互運用を容易にするための言語機構の研究を行った．具体的にはML言語に対する Ohori による多相レコードのための型システムとコンパイル方式を拡張することで、レコードとハッシュテーブルの相互運用を許す型システムと型推論アルゴリズムを構築した．そして、低級言語へのコンパイル方式を考案した．この内容はプログラミングおよびプログラミング言語ワークショップ(2021年3月)でポスター発表を行った．その際、多相レコードをサポートするSML#言語のコンパイラ開発者と議論し、この方式がSML#上に実装可能である見通しを得た．
【研究項目2. 多言語モジュールで構成されたソフトウェアシステムの検証機構】については、System F流のパラメトリック多相型システムに対する漸進的型付け拡張の性質を研究した．特に、素朴な実行検査方式では空間計算量を悪化させる可能性がある問題に着目して、漸進的多相型システムでこの問題がどうなるかを検討した．その結果として、従来提案されてきた空間効率改善手法が、漸進的多相型システムでは適用不可能であることを理論的に示すことができた．この結果は、Scheme and Functional Programming Workshop (2021年9月)において口頭で発表を行った．
|
| 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にも有益な結果であり、総合的にはおおむね順調に進展したと判断している．
|
| Strategy for Future Research Activity |
新型コロナウイルス感染症の問題は続いており、海外からのポスドク研究員雇用は令和4年に入ってようやく環境が整ってきたため、速やかに進めたい．また、レコードとハッシュテーブルの相互運用技術は、SML#コンパイラの上に実装を進めるが、大規模なソフトウェアの改造を伴うため、研究協力者を増強することを考えたい．
|
