2018 Fiscal Year Annual Research Report
New reational program semantics based on the notion of continuations and contexts
| Project/Area Number |
16K12409
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 継続 / 評価文脈 / 環境双模倣 / call/cc / λ計算 / 名前呼び・必要呼び / セキュリティ型 / 条件分岐・if文 |
|---|
| Outline of Annual Research Achievements |
本研究の目的は、「残りの計算」を表す概念である継続(continuation)と、「現在実行中のプログラムのまわりのプログラム」を表す評価文脈(evaluation context)の概念に基づく、新たなプログラミング言語理論の確立である。
当年度は前年度までに得られた、call-with-current-continuation（call/cc，継続を操作する演算子の一つ）を持つλ計算（関数型プログラミング言語の理論的体系）のための新たな双模倣（bisimulation，異なるプログラムの等価性を証明する手法の一つ）の理論に続き、評価文脈の概念と密接に関連する、名前呼び(call-by-name)評価と必要呼び(call-by-need)評価の対応に関する研究に取り組んだ。
特に、名前呼び評価と必要呼び評価の対応を定理証明支援器で定式化するにあたり、従来よりも扱いが容易な対応関係を考察・着想し、より初等的（操作的）でありながら厳密な証明を得た。
また、データの機密度を型として表すセキュリティ型付きλ計算という理論体系において本質的に問題となる条件分岐（if文）の扱いに評価文脈の考え方を適用し、問題を解決する新たな糸口を得た。
これらの研究は研究協力者ら（事務上、分担金の配分を必要とせず研究分担者とならない同一研究室の研究者や、研究者番号を持たず研究分担者になれない同一研究室の博士後期課程学生・博士前期課程学生・学部4年生（いずれも研究実施当時）を含む）との共同研究である。
|
