2020 Fiscal Year Annual Research Report
安全・高信頼ソフトウェアシステムのための高階・型付き・並行プログラミング言語理論
| Project/Area Number |
20H04161
|
|---|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2020-04-01 – 2025-03-31
|
| Keywords | プログラミング言語理論／プログラム理論 / 高階・並行・分散計算 / 型システム / 関数型プログラミング／関数型プログラミング言語 / プログラミング言語理論に基づくセキュリティ |
|---|
| Outline of Annual Research Achievements |
研究の目的：現代社会の基盤をなす科学技術である情報処理システム（いわゆる計算機プログラムを基礎とするが，それに限らず，より幅広い意味でのソフトウェアシステムを含む．）の安全性・信頼性ならびに生産性を高めるため，数理論理学に基づいてシステムを記述し正しさを検証するプログラミング言語理論を発展させ，狭義のプログラミング言語のみならず，より一般的な計算モデルにおける広義の「プログラム」としてのシステム記述に用いる．特に，最近の発展・普及が目覚ましい，高度な型システムや高階(higher-order)および並行(concurrent)・分散プログラムないしプログラミング言語に関する理論の研究を行う．本研究により，代表者らが国際的に高く評価されているプログラミング言語理論を中心とする理論計算機科学・情報科学の発展，ひいては情報処理システムの安全性・信頼性・生産性の向上につながることが期待される．
当該年度（繰越前および繰越後）は，プログラミング言語理論の中でも特に「高階」「並行・分散」「型システム」の（相互に強く関連する）３点を軸として，例えば以下のような研究を行った．１．型システムによるロックフリーアルゴリズムとデータ構造の検証，２．未完成のプログラムの多相的漸進的型付けと部分的実行の理論，３．自律型ロボットへの型付き高階関数型メタプログラミングの応用，４．定理証明支援器や自動定理証明器によるアルゴリズムの計算量や高階関数の等価性の検証．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
繰越前の年度は複数の発表を行なった．繰越後の年度は，まだ発表には至っていないが，新たなサブテーマを含め，複数の研究が進展した．
|
| Strategy for Future Research Activity |
申請書に明記して採択されたとおり，本研究は学術的基礎研究であり，すべての研究内容の具体的詳細を事前に計画することは本質的に不可能だが，引き続き計画に従って研究を推進する．
|
