| Project/Area Number |
16K12409
|
|---|
| Research Category |
Grant-in-Aid for Challenging Exploratory Research
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
Sumii Eijiro 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Research Collaborator |
Matsuda Kazutaka
Kiselyov Oleg
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2018: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2017: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2016: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
|---|
| Keywords | 継続 / （評価）文脈 / プログラム等価性 / call/cc / λ計算 / （環境）双模倣 / 評価文脈 / 環境双模倣 / 名前呼び・必要呼び / セキュリティ型 / 条件分岐・if文 / 必要呼び / 名前呼び / 遅延評価 / 評価戦略 / Call/cc / 継続演算子 / プログラミング言語理論 / プログラム理論 / ソフトウェア基礎 / 継続(continuation) |
|---|
| Outline of Final Research Achievements |
A theory for proving program equivalence, based on environmental bisimulations, has been developed in a foundational calculus modelling a functional programming language with the undelimited continuation operator "call/cc" (call-with-current-continuation).
|
| Academic Significance and Societal Importance of the Research Achievements |
現代社会において計算機を中心とする情報処理システムの重要性は言をまたないが、多くの計算機ソフトウェアの理論的基礎は薄弱であり、毎日のように「不具合」（という名の誤動作）を起こして社会的問題となっている。本研究のような「プログラミング言語理論」は、狭義の「プログラム」のみならず、広義の「計算モデル」も含め、数理論理学的基礎による堅固な理論の確立・発展・応用を目指している。本研究もその一つであり、前述の「継続」と「文脈」という、広義の計算機プログラムにおいて重要な概念を扱った、「二つのプログラムの動作が等しい」という基本的な性質を証明する手法の成果である。
|
