1997 Fiscal Year Final Research Report Summary
Theory of Constructive Programming
| Project/Area Number |
08458068
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
SATO Masahiko Kyoto Univ.Information Science Prof., 工学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKEUTI Izumi Kyoto Univ.Information Science.Instructor, 工学研究科, 助手 (20264583)
KAMEYAMA Yukiyoshi Kyoto Univ.Information Science.Assoc.Prof.Instructor, 工学研究科, 助教授 (10195000)
TATSUTA Makoto Kyoto Univ.Math.Assoc.Prof., 理学研究科, 助教授 (80216994)
|
|---|
| Project Period (FY) |
1996 – 1997
|
| Keywords | Constructive Programming / Catch / Throwcontrd / Type Theory |
|---|
| Research Abstract |
This project had three large subjects, which are listed in the following.
The first was to construct logical systems corresponding to catch-throw mechanism. The investigators researched for characteristics and semantics of logical systems corresponding to catch/throw mechanism. As the result of that the investigators constructed the logical systems MJct and NKct, and proved that the logical systems NJct and NKct are conservative extensions of NJ and NK, respectively. The investigators also showed that these systems are useful for constructive programming. This subject was mainly developed by Sato and Kameyama.
The second was on realizability interpretations of untyped calculation theory. The investigations was aimed at giving realizability interpretations for logical systems with untyped calculus, and applying it to constructive programming. As the result of that, the investigators gave a realizability interpretation for logical system for a set theory. This realizability interpretation is very much improved as compared to the former ones, which used double variables. The investigators also gave a realizability interpretation for a system with co-induction, and showed an application of this realizability interpretation to constructive programming. This subject was mainly developed by Tatsuta.
The third was on constructivew logical systems for polymorphism. The investigators made a research pn parametricity of polymorphic calculation systems, such as SYstem F, second order lambda calculus. As the result of that, the investigators gave logical systems ; one of them is for parametric polymorphism of System F, and another is for cyclic structure. This subject was mainly developed by Takeuti.
|
