2008 Fiscal Year Annual Research Report
| Project/Area Number |
18680003
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 Tohoku University, 大学院・情報科学研究科, 准教授 (00333550)
|
|---|
| Keywords | プログラミング言語 / 計算モデル / λ計算 / π計算 / 操作的意味論 / 文脈等価性 / 双模倣 / 論理関係 |
|---|
| Research Abstract |
λ計算やπ計算といった数理論理学的計算モデル・プログラミング言語モデルにおいて、その言語モデルの任意の文脈下での等価性(文脈等価性)や時間・空間性能改善、メモリ安全性といった「文脈的性質」を証明するための基礎理論を確立した。この基礎理論は研究代表者らがすでに提案した環境双模倣(environmental bisimulation)を拡張・一般化するもので、論理関係(logical relation)などの従来手法に比べ、メモリ解放や並行プリミティブ等を有する、より現実的な計算体系にも容易に適用できる。本理論はプログラミング言語基礎研究における国際的著名学会European Symposium on Programmingにて、ほぼ最高に近い評価を得て採択・発表された。
また、従来の理論では取り扱いの難しかった、破壊的代入の可能な参照セル(reference cell)と多相・抽象データ型(polymorphic/abstract data type)とを同時に有するλ計算や、プロセス自身を通信する高階プロセス(higher-order process)と暗号プリミティブとを同時に有するπ計算においても環境双模倣の理論を構築、正式な論文としては未発表であるにも関わらず、すでに国外の主要な研究者らから高い関心が寄せられている。
さらに、環境双模倣や論理関係を含む各種証明手法の直観的関連や数理論理学的比較に関して国外の第一線研究者らと議論し、今後の新たな研究に結びつく知見を得た。
並行して、国内の論文誌編集者の依頼により、強い静的型付け(strong static typing)に基づく安全なプログラミング言語MLの教育用サブセットコンパイラMinCamlに関する和文論文を執筆・投稿し、やはり高い評価を得て一回の査読により採択された(通常は1〜2回の照会を経ることが多い)。
|
