Co-operative research on foundational theories of programs

我们学习了（1）数学基础，（2）应用数学和（3）编程。构建了程序设计的基础理论，研究了基于这些理论的软件开发方法，开发了实际的应用软件。通过对各种程序设计基础理论的研究，探讨这些理论之间的关系，加深了对这些理论的认识。特别地，Sato构造了一个以证明为内部对象的逻辑系统RPT，为程序理论奠定了基础。龙田研究了构造性编程的归纳定义的可实现性解释。龟山实现了一个构造性的程序设计系统，并研究了计算机网络，这为研究奠定了基础。伊藤研究了并发进程和项重写系统的结构化模型，并根据实验结果实现了软件。Hayashi提出了一种新的类型理论框架，通过单例，并和交叉类型，并表明它是更好的表达比其他框架的构造性编程。Hagiya研究了实现用于描述形式证明的计算机环境的基本技术，例如证明检查器的用户界面，其中包括通过示例和可视化证明的证明。Ono研究了没有结构规则的逻辑语义、决策问题和有限模型属性。Noshita开发了游戏树的快速搜索技术，并将其应用于解决Tsume-shogi的软件。Ushijima研究了并发程序测试和调试方法的基本理论和实际实现。

We have studied (1) mathematical foundations,(2) applied mathematics and (3) programming. We have constructed foundational theories of programming,researched methods of software development based on the theories and developed actual application software. By studying variety of foundational theories of programming and discussing relationship among these theories, We have deepened knowledge about these theories. Particularly the research have got the following results.Sato constructed a logical system RPT, which has proofs as internal objects and gave foundations of theory of programs. Tatsuta studied realizability interpretations of inductive definitions for constructive programming. Kameyama implemented a constructive programming system and studied computer network, which gives infrastructures of the research. Ito studied structured models of concurrent processes and term rewriting systems and implemented software based on the results as an experiment. Hayashi presented a new framework of type theories by singleton, union and intersection types and showed that it is more expressive for constructive programming than other frameworks. Hagiya studied basic techniques to implement computer environment for describing formal proofs, such as user interfaces of a proof checker which include proofs by examples and visualization of proofs. Ono studied semantics of logics without structural rules, decision problems and finite model properties. Noshita developed fast search techniques for game trees and applied it to software which solves Tsume-shogi. Ushijima studied foundational theories and actual implementation of testing and debugging methods of concurrent programs.