| 研究概要 |
(1)高須はIFIP86の大会におけるパネル討論においてパネリストとしてプログラム演繹合成法の現状と将来について意見を述べた. (2)補題の証明と補題の適用ての関係をカット消去法を用いて調べ結果としてレソリュション法における証明構成過程で必要な補題を探す発見手法を提案することが出来た.
(3)林は構成的推論体系PXを提案し, その体系のなかでプログラム演繹合成法を展開すると共に型理論の基礎付けを論じた. またこの体系を基礎とするプログラム合成システムの開発についても報告している.
(4)萩谷はKCLと呼ばれるCommon Lispシステムを開発したこのシステムは移植性が極めて高く, またコンパイラの性能も極めて良いので現在世界中で使用されるようになって来ている.
(5)萩谷は, 既存の具体的なプログラムを一般化し抽象的なプログラムスキーマを構成する方法に関して, プログラムを高階型理論の項として表現し, プログラマが指定したパラメータをwelltypedなスキーマへ拡張する問題として定式化し, 最大の一般化を求める手続を与えている.
(6)萩谷は拡張可能でネットワーク・ワイドなマルチウインドシステムを開発した.
(7)萩谷はメタ・サーキュラなインタプリタを通じて型の体系が定義される関数型言語の理論を展開した. この論文は萩谷の学位論文である.
|
