1986 Fiscal Year Annual Research Report
| Project/Area Number |
60580024
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
高須 達 京大, 数理解析研究所, 教授 (10027360)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
中原 敬子 京都大学, 数理解析研究所, 教務員 (90155797)
萩谷 昌己 京都大学, 数理解析研究所, 助手 (30156252)
林 晋 京都大学, 数理解析研究所, 助手 (40156443)
|
|---|
| Keywords | 定理の証明 / プログラム検証 / プログラム合成 / 型付関数型言語 |
|---|
| Research Abstract |
〔1〕プログラムの検証と合成とを自動的に行なうためのシステムPXの開発を完成し、情報処理学会国際連合第2.2研究委員会主催の国際会議において発表を行った。(林 晋)
〔2〕情報処理学会国際連合の1986世界大会において、パネル討論者としてProgramming=Theory Formation and Theory development
Programming Language=Formal System
Specification=Conjectured Theorem
Sequential Program=Constractive Proof
Coding=Proving
という知見について討論を行った。(高須 達)
〔3〕述語論理LK,LJからresolutionによる証明システムへの変換を考察し、Prologプログラムを仕様のLK,LJにおける証明から抽出する方法を得ることが出来た。(高須 達)
〔4〕多重型付関数型言語を設計し、それによるメタ・サーキュラーなインタプリンターを作製した。
|
-
[Publications] 林晋: Proceedings of the 3rd Working Conference on the Formal Description of Programming Concepts. (1986)
-
[Publications] 高須達: Information Processing 86. 398-398 (1986)
-
[Publications] 高須達: 日米セミナー. (1987)
-
[Publications] 萩谷昌己: 日本ソフトウェア科学会 第3回論文集. (1986)
