安全・高信頼ソフトウェアシステムのための高階・型付き・並行プログラミング言語理論
| Project/Area Number |
23K20379
|
|---|
| Project/Area Number (Other) |
20H04161 (2020-2023)
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Multi-year Fund (2024)
Single-year Grants (2020-2023) |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2024)
|
| Budget Amount *help |
¥17,680,000 (Direct Cost: ¥13,600,000、Indirect Cost: ¥4,080,000)
Fiscal Year 2024: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2023: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2022: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2021: ¥3,510,000 (Direct Cost: ¥2,700,000、Indirect Cost: ¥810,000)
Fiscal Year 2020: ¥6,500,000 (Direct Cost: ¥5,000,000、Indirect Cost: ¥1,500,000)
|
|---|
| Keywords | プログラミング言語理論／プログラム理論 / 高階・並行・分散計算 / 型システム / 関数型プログラミング／関数型プログラミング言語 / プログラミング言語理論に基づくセキュリティ |
|---|
| Outline of Research at the Start |
プログラミング言語理論の中でも特に「高階」「並行・分散」「型システム」の（相互に強く関連する）３点を軸として、以下のような研究を行う。（基金化前を含む当初の計画であり、「科学研究」「基盤研究」の本質として、研究の発展にともない、本研究課題に関するさらなる新しい理論にも取り組む可能性もある。）１．非機密化操作を備えたセキュリティ型つきλ計算のための環境双模倣による機密性・等価性証明手法、２．暗号化・復号機能と状態を有するネットワーク記述・検証体系、３．高階プログラム検証のための自動定理証明、４．型システムによるロックフリーアルゴリズムとデータ構造の検証、５．遅延評価の意味論と実装の形式化と検証。
|
| Outline of Annual Research Achievements |
本研究の目的は以下のとおりであった。現代社会の基盤をなす科学技術である情報処理システム（いわゆる計算機プログラムを基礎とするが、それに限らず、より幅広い意味でのソフトウェアシステムを含む。）の安全性・信頼性ならびに生産性を高めるため、数理論理学に基づいてシステムを記述し正しさを検証するプログラミング言語理論を発展させ、狭義のプログラミング言語のみならず、より一般的な計算モデルにおける広義の「プログラム」としてのシステム記述に用いる。特に、最近の発展・普及が目覚ましい、高度な型システムや高階(higher-order)および並行(concurrent)・分散プログラムないしプログラミング言語に関する理論の研究を行う。
当年度は以下を含む研究を研究協力者らとともに、他の研究とも連携して行なった。
・構造化グラフの正規化の証明：関数的(functional)な表現が難しいとされるグラフ構造を関数的に表現する手法の一つであるOliveira-Cookの構造化グラフ(structured graph)において、表現（項）の冗長性を取り除くための正規化(normalization)の規則を定義・証明した。
・複数参加者セッション型の一般プロセス型への変換：複数の参加者（プロセス）が通信を行う並行プロセス計算(concurrent process calculus)において、通信のプロトコル（順序等の手順）を表すセッション型(session type)から、プロセスの入出力の振る舞いを表すIgarashi-Kobayashiの一般型システム(generic type system, GTS)への変換を定義し、両者の関係を明らかにした。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
大学・部局の事務職員・技術職員の不足により、教員が多くの事務・施設管理等業務や業者への対応等を行わなければならず、極めて長時間の努力をもってしても研究時間がほとんど確保できなかった。
|
| Strategy for Future Research Activity |
大学・部局の事務職員・技術職員の不足は一研究者で直ちに対応はしがたいが、引き続き研究時間の確保に最大限努力しつつ、遅れてはいるが当初の計画に沿って研究を遂行する。
|
Report
(2 results)
Research Products
(8 results)
