The new aspects in constructive programming.

(1)利用catch/throw逻辑对PX系统进行了扩展，并研究了其与非信息量词的关系。我们利用PX的CIG归纳方案的“框架”概念，将中野的catch/throw逻辑添加到构造性编程逻辑中。我们用中野逻辑实现了PX的原型，并进行了实验。由于PX系统的逻辑是基于Lisp系统的，因此无法知道在计算中是否发生了抛出。我们证明了这种观察是由Hayashi的非信息量词自然形式化的。(2)引入了非确定性的catch/throw机制。它自然地引入了非确定性计算。我们给出了一个理论，表明这种非确定性机制不会导致逻辑矛盾。(3)给出了与S4模态逻辑相对应的构造逻辑。论证了它的可实现性与莫吉斯单一性类型论中的崩溃在本质上是一致的。我们证明了评价模态可以看作是非信息量词的扩展，它增加了模态逻辑的可表达性。(4)除上述主要结果外，我们还得到了以下结果：(1)实现了另外两个版本的PX系统，一个是基于多值计算的，另一个是有很大改进的用户界面。（ii）完善了PX的逻辑基础，并将其与Frege结构联系起来。

(1) We extended PX system by catch/throw logic and investigated its relation to non-informative quantifiers. We added catch/throw logic by Nakano to constructive programming logic using the concept of "frame" of CIG induction scheme of PX.And we implemented a prototype of PX with Nakano logic and conducted experiments with it. As the logic of PX system is based on Lisp system, there is no way to know weather a throw occuerd in a computation. We showed this observation is naturally formalized by the non-informative quantifiers by Hayashi.(2) We introduced the non-deterministic catch/throw mechanism. It naturally introduces non-deterministic computation. We gave a theory which shows such a non-deterministic mechanism does not lead to contradiction of the logic.(3) We gave a constructive logic correspoinding to S4 modal logic. We showed that its realizability and Moggis's collapsing in his monad type theory are essentially the same. We showed that the evaluation modality can be counted as an extension of non-informative quantifier and it increases the expressivility of the modal logic.(4) Besides the main results above, we got the following results : (i) two other versions of PX system were implemented, one is based on multiple value computation and the other has a much improved user interface. (ii) we improved the logical foundation of PX and related it to Frege structure.