Project/Area Number 
08458068

Research Category 
GrantinAid for Scientific Research (B)

Allocation Type  Singleyear Grants 
Section  一般 
Research Field 
計算機科学

Research Institution  KYOTO UNIVERSITY 
Principal Investigator 
SATO Masahiko Kyoto Univ.Information Science Prof., 工学研究科, 教授 (20027387)

CoInvestigator(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

Project Status 
Completed (Fiscal Year 1997)

Budget Amount *help 
¥7,300,000 (Direct Cost: ¥7,300,000)
Fiscal Year 1997: ¥2,600,000 (Direct Cost: ¥2,600,000)
Fiscal Year 1996: ¥4,700,000 (Direct Cost: ¥4,700,000)

Keywords  Constructive Programming / Catch / Throwcontrd / Type Theory / Catch / Throw機構 
Research Abstract 
This project had three large subjects, which are listed in the following. The first was to construct logical systems corresponding to catchthrow 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 coinduction, 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.
