1994 Fiscal Year Annual Research Report
| Project/Area Number |
06680333
|
|---|
| Research Institution | Ryukoku University |
|---|
Principal Investigator |
林 晋 龍谷大学, 理工学部, 教授 (40156443)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小林 聡 龍谷大学, 理工学部, 助手 (60195831)
中野 浩 龍谷大学, 理工学部, 助手 (30217799)
|
|---|
| Keywords | 構成的プログラミング / 形式的方法 / 型理論 / 構成的数学 |
|---|
| Research Abstract |
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)の仕様記述に役立つことを発見した。(林,中野,小林)
|
-
[Publications] S.Hayashi: "Logic of refinement types" Springer Lecture Notes in Computer Science. 806. (1994)
-
[Publications] S.Hayashi & S.Kobayashi: "A new formalization of Feferman's system of functions and classes and its relation to Frege structure" International Journal of Foundations of Comp.Sci.(to appear)(accepted).
