2009 Fiscal Year Annual Research Report
| Project/Area Number |
18500005
|
|---|
| Research Institution | Ochanomizu University |
|---|
Principal Investigator |
浅井 健一 Ochanomizu University, 大学院・人間文化創成科学研究科, 准教授 (10262156)
|
|---|
| Keywords | 部分継続 / プログラム理論 / 情報基礎 |
|---|
| Research Abstract |
本年度は最終年度ということで、これまでの研究内容をさらに発展させるとともに、研究成果の発表にも力を入れた。1.型システムの基本的な性質について、Isabelle/HOLのNominalパッケージを用いて証明を試みたが、名前の付け替えに関してNominalパッケージを使っても解決が難しい問題があることが分かり、それを学会にて報告した。2.functional derivationの手法を使って、継続計算の定義と等価な仮想機械を導出した。この仮想機械はスタックへの値の退避や、スタックコピーをモデル化しており、実質的に機械語による限定継続の実装が正しいことを保証するものとなっている。その内容について学会で発表し、論文賞を受賞した。3.限定継続を使用しても例外解析を行うことは可能だが、それによって得られるものがほとんどなさそうなことがわかった。一方、限定継続の応用であるprintfについては、その仕様から系統的に実装を導くことに成功した。また、printfの双対と考えられるscanfについても同様の結果を導いた。4.昨年度に作成した限定継続命令の直接実装法をより現実的なプログラミング言語Caml Lightに適用し、その結果として、実用的な言語に限定継続を直接実装することに成功した。これで限定継続を使った各種のプログラムを自在に実行できる環境が整ったことになる。5.限定継続の基礎体系として対称ラムダ計算についての研究を進めた。特にWadlerの双対計算との間の変換を定義し、それぞれの等式理論が保存されることを示した。これは同時に対称ラムダ計算が古典論理に対応することも示したことになる。
|
