Theory of Constructive Programming

这个项目有三个大课题，列在下面。首先是构建与catch-throw机制相对应的逻辑系统。研究了与接/扔机制相对应的逻辑系统的特征和语义。在此基础上构造了逻辑系统MJct和NKct，并证明了逻辑系统NJct和NKct分别是NJ和NK的保守扩展。研究人员还表明，这些系统对建设性规划是有用的。这一学科主要由佐藤和龟山发展起来。二是关于非类型化计算理论的可实现性解释。研究的目的是给出具有无类型微积分的逻辑系统的可实现性解释，并将其应用于构造规划。在此基础上，研究者给出了集合论逻辑系统的可实现性解释。与以前使用双变量的解释相比，这种可实现性解释有了很大的改进。研究人员还给出了共归纳系统的可实现性解释，并展示了这种可实现性解释在构造规划中的应用。这门学科主要是由Tatsuta开发的。第三篇是关于多态的构造逻辑系统。对系统F、二阶λ演算等多态计算系统的pn参数性进行了研究。结果，调查者给出了逻辑系统；其中一个是系统F的参数多态性，另一个是循环结构。该学科主要由竹井开发。

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.