| Project/Area Number |
60580024
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
TAKASU Satoru Research institute for mathematical Sciences, 数理解析研究所, 教授 (10027360)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
NAKAHARA Takako ibid, 数理解析研究所, 教務員 (90155797)
HAGIYA Masami ibid, 数理解析研究所, 助手 (30156252)
HAYASHI Susumu ibid, 数理解析研究所, 助手 (40156443)
|
|---|
| Project Period (FY) |
1985 – 1987
|
| Project Status |
Completed (Fiscal Year 1987)
|
| Budget Amount *help |
¥2,400,000 (Direct Cost: ¥2,400,000)
Fiscal Year 1987: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1986: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1985: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | Program synthesis / intuitionistic predicate calculus / type theory / LISP generalizatin of programs fuctional language / プログラムの一般化 / マルチウィンドウシステム / 関数型言語 / 定理の証明 / プログラム検証 / 型付関数型言語 |
|---|
| Research Abstract |
(1) Takasu gave an address in a panel discussion of IFIP '86 Congress as a panelist, on the present and future of deductive program synthesis.
(2) Takasu studied a relation between a proof of a lemma and a proof involving an application of the lemma in the resolution method using the cut eliminatin method. As a result he obtained a heuristic method to find out a necessary lemma during a construction of some proposition in resolutin method.
(3) Hayashi proposed a constructive predicate logic PX, in which he disscussed a mthod for deductive program synthesis.
(4) Hagiya has limplemented a common Lisp system which is portable for wide variety of computers and is very efficient.
(5)Hagiya developped a theory on the genelarization of programs by parametrizatin in higher order type theory.
(6) Hagiya established a theory of a functional language in which its type system is defined through a meta-circular interpreter.
|
