| 研究課題/領域番号 |
23K20379
|
|---|
| 補助金の研究課題番号 |
20H04161 (2020-2023)
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 基金 (2024)
補助金 (2020-2023) |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2024年度)
|
| 配分額 *注記 |
17,680千円 (直接経費: 13,600千円、間接経費: 4,080千円)
2024年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2023年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2022年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2021年度: 3,510千円 (直接経費: 2,700千円、間接経費: 810千円)
2020年度: 6,500千円 (直接経費: 5,000千円、間接経費: 1,500千円)
|
|---|
| キーワード | プログラミング言語理論／プログラム理論 / 高階・並行・分散計算 / 型システム / 関数型プログラミング／関数型プログラミング言語 / プログラミング言語理論に基づくセキュリティ |
|---|
| 研究開始時の研究の概要 |
プログラミング言語理論の中でも特に「高階」「並行・分散」「型システム」の（相互に強く関連する）３点を軸として、以下のような研究を行う。（基金化前を含む当初の計画であり、「科学研究」「基盤研究」の本質として、研究の発展にともない、本研究課題に関するさらなる新しい理論にも取り組む可能性もある。）１．非機密化操作を備えたセキュリティ型つきλ計算のための環境双模倣による機密性・等価性証明手法、２．暗号化・復号機能と状態を有するネットワーク記述・検証体系、３．高階プログラム検証のための自動定理証明、４．型システムによるロックフリーアルゴリズムとデータ構造の検証、５．遅延評価の意味論と実装の形式化と検証。
|
| 研究実績の概要 |
本研究の目的は以下のとおりであった。現代社会の基盤をなす科学技術である情報処理システム（いわゆる計算機プログラムを基礎とするが、それに限らず、より幅広い意味でのソフトウェアシステムを含む。）の安全性・信頼性ならびに生産性を高めるため、数理論理学に基づいてシステムを記述し正しさを検証するプログラミング言語理論を発展させ、狭義のプログラミング言語のみならず、より一般的な計算モデルにおける広義の「プログラム」としてのシステム記述に用いる。特に、最近の発展・普及が目覚ましい、高度な型システムや高階(higher-order)および並行(concurrent)・分散プログラムないしプログラミング言語に関する理論の研究を行う。
当年度は以下を含む研究を研究協力者らとともに、他の研究とも連携して行なった。
・先進的かつ実用的なプログラミング言語として産業界の技術者にも注目され普及している「Rust」の最も特徴的な機能である「所有権」(ownership)にもとづくメモリ管理について、既存のRustの所有権検査器(borrow checker)および参照カウント(Rc)オブジェクトでは静的（コンパイル時）検査も動的（実行時）検査も十分でないケースを考え、そのような場合でも静的検査と動的検査を適切に組み合わせて安全かつリークを防ぐ、分数的(fractional)所有権にもとづくメモリ管理方式を提案・実装した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
前年度と同様の理由に加え、当年度は教育（学生指導）の負担も極めて大きかったが、バイアウト等の制度を活用して改善の方向にある。
|
| 今後の研究の推進方策 |
引き続きバイアウト等の制度を活用して、研究時間の確保に最大限努力しつつ、遅れてはいるが当初の計画に沿って研究を遂行する。
|
