| Project/Area Number |
18K11156
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
Asada Kazuyuki 東北大学, 電気通信研究所, 助教 (00570251)
|
|---|
| Project Period (FY) |
2018-04-01 – 2022-03-31
|
| Project Status |
Completed (Fiscal Year 2021)
|
| Budget Amount *help |
¥2,860,000 (Direct Cost: ¥2,200,000、Indirect Cost: ¥660,000)
Fiscal Year 2020: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2019: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2018: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 関数型プログラミング言語 / 表示的意味論 / 完全抽象モデル / プログラム検証 / 線形論理 / 量子プログラミング言語 / 圏論 / 交差型 / ゲーム理論 / 高階プログラム検証 / 高階不動点論理 / 圏論的意味論 / 線形代数 / 量子プログラミング / ゲーム意味論 / モデル検査 / 非決定計算 / 関数型言語 / ラムダ計算 / 高階文法 / 確率計算 / 量子計算 / 反復補題 / プログラミング言語 / 普遍的モデル / 多相型 / 再帰型 |
|---|
| Outline of Final Research Achievements |
Our work provides useful models of programming languages equipped with complex computational effects in a general framework. Among these, the model of a functional quantum programming language analyzes a new aspect of the quantum computational effect. This semantic evolution opens many technical challenges, provides ideas to solve them, and makes great progress of the research area.
We also studied an application of our theoretical techniques to model checking, and obtained a new algorithm with an implementation.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究で得られたプログラミング言語の表示的意味論の成果は，分野のまとまった成果を一般性を持って再構成するものであり，新しい長期的な視点を分野に提供するものであり，今後の意味論分野の発展に大きく寄与するものである．また量子計算の機構を備えた関数型プログラミング言語は今後ますます重要となるものであり，その意味論的成果は大きく社会に資する研究である．本研究の意味論的技術はモデル検査などへの応用も期待でき，ソフトウェア工学的にも価値の高い技術である．
|
