Theory of Constructive Programming

点击翻译按钮获取中文摘要

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.