Co-operative research on foundational theories of programs

我们学习了(1)数学基础，(2)应用数学和(3)规划。构建了程序设计的基础理论，研究了基于这些理论的软件开发方法，并开发了实际的应用软件。通过学习规划的各种基本理论，并讨论这些理论之间的关系，我们加深了对这些理论的认识。佐藤构建了一个以证明为内在对象的逻辑系统RPT，为程序论提供了理论基础。Tatsuta研究了建构性规划归纳定义的可实现性解释。龟山实现了一个建设性的编程系统，并研究了计算机网络，这为研究提供了基础设施。ITO研究了并发进程和术语重写系统的结构化模型，并根据结果实现了软件作为实验。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.