2021 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. モジュール間のデータ変換機構とその自動化の研究】前年度から行っているレコードとハッシュテーブルが相互運用な可能な言語の研究を進め，基本的な機能をSML#コンパイラ上に実装することができ，この成果について国内研究集会で論文発表を行った．一方で，SML#に実装されているOhoriの多相レコード計算の制限から再帰的データ構造の取り扱いに当初想定していなかった問題があること，ならびにコンパイラ内での中間処理に起因する制限から，ある種類のプログラムについてはうまくコンパイルできないことが判明した．前者について，解決の方策は既に得られているが理論的な問題がないことを確認する必要がある．後者については純粋にエンジニアリング的な問題であり時間をかければ解決可能であると見込んでいる．一般的なデータ変換の自動化機構については関連研究のサーベイなどを行った．
また、関連して、LLVM IR からスマートコントラクト言語Michelsonへのコンパイル方式の研究を行った。これは多言語モジュールでスマートコントラクトを記述することにも繋がる。
【研究項目2. 多言語モジュールで構成されたソフトウェアシステムの検証機構】交付申請書であげた(項目2-1)については，項目1のデータ変換自動化機構とも密接に関連することもあり，関連研究のサーベイに費した．
(項目2-2)の多相型を持つ言語と動的型付言語間の相互運用を行うための実行検査については，前年度までの空間効率のよい実装の不可能性の理論的結果に基づき，不可能性がパラメータ性を実行時に保証するために使われている名前生成機構のみに因ることを理論的に示した．具体的には，空間効率の指標となるサイズ関数の定義を，連続したコアーションについてはサイズを定数と見做すことにすれば，空間効率がよいと見做せることを証明した．
|
| 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)，そしてやや遅れているものが混在しているが、全体的には「おおむね順調」と判断した。遅れている項目は研究項目1と2-1の一般的なモジュール間データ変換機構とその検証機構であるが，新型コロナウイルス感染症拡大の影響はまだ大きく，予定していたポスドク研究員の雇用がままならないままであることが主要な原因である．
|
| Strategy for Future Research Activity |
ポスドクについては雇用の目処がたっており，遅れている項目について加速したい．また，レコードとハッシュテーブルの相互運用のコンパイラ実装については，基本的な部分は動作しているが，担当していた研究協力者の大学院生の修了の穴を埋め完成度の向上を目指す。
|
