2010 Fiscal Year Annual Research Report
| Project/Area Number |
21300005
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
亀山 幸義 筑波大学, システム情報工学系, 教授 (10195000)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
浅井 健一 お茶の水女子大学, 大学院・人間文化創成科学研究科, 准教授 (10262156)
五十嵐 淳 京都大学, 大学院・情報学研究科, 准教授 (40323456)
|
|---|
| Keywords | コード生成 / マルチステージプログラミング / 型システム / 様相論理 / コントロールオペレータ / 型エラー / Curry-Howardの対応 |
|---|
| Research Abstract |
本研究の目的は、コード生成のためのプログラミング言語であるマルチステージ言語の基礎となる計算体系の確立である.
今年度の研究では、計算エフェクトを利用するための機構を持つ型付きマルチステージ言語を設計し、その型システムの健全性を証明した。本言語に含まれる計算エフェクトは、タグ付き限定継続(delimited continuation)と呼ばれるものであり、このエフェクトをプログラムの中から利用できるコントロールオペレータを持つことにより、精密で高性能なコードを生成することが可能となった。型システムの健全性により、生成されたコードが型安全性で、かつ、自由変数が発生しないという性質が導かれるため、本言語を利用したコード生成は高い安全性・信頼性を持つと言える。また、MetaOCamlなどのマルチステージプログラム言語の基礎となる体系λαを論理学的見地から見直し、より簡潔で表現力が十分強力である体系を設計し、その基礎理論を確立した。
マルチステージプログラム言語の安全性が型システムに依拠していることから、関連研究として、型の導出をヴィジュアルに行うためのシステムの設計を行った。また、型エラーが起きた場合、通常のシステムでは、型エラーの原因となる部分から遠く離れた部分を指摘するエラーメッセージが表示されたり、必要以上に多くの情報が表示されたりする事が頻繁に起きるが、Wellsらの型エラー・スライスに基づく手法を改善して、型エラーの原因に関係する部分のみを適切に表示するアルゴリズムを設計・実装した。
|
