| 研究概要 |
1.vefinement typeの理論ATTTの操作的意味論(仏INRIAのB.Werner氏との共同研究)(林)
2.catch/throw ニカニズムの論理の意味論を、項書き換えシステムにより、再度基礎づけた。これにより非決定的計算を取り込める。(中野)
MoggiのMonadを記述するEvaluation Logicのconstuctive versionの定義とrealizability。(小林)
4.PXのCommonLispへの移植と、その拡張。
拡張1.プログラムに完全な仕様がattachされていることを利用し、不必要なリストの生成を自動的に削除する方法を与えた。そして、このアイデアをもとに、mvPXを作成した。mvPXはリストを多値でおきかえる。これにより、2〜4倍の効率の向上が得られた。(林)
拡張2.PXに中野のcatch/throw論理のメカニズムを追加した。そして、そのアイデアをもとにctPXを作成した。これにより構成的プログラミングの枠内で、非局所的脱出を行なうプログラムの初の合成に成功した。また、PXのような型のないシステムの場合、ATTTのnon-informative演算子が、非局所的脱出(catch/throw)の仕様記述に役立つことを発見した。(林,中野,小林)
|
