Implementation of Distributed Programming Languages Based on Advanced Theory for Concurrent/Distributed Computation

该研究项目的最初目标是设计和实现基于并发/分布式计算的先进理论基础的分布式编程语言。在进行这项研究的同时，我们面临着进一步扩展并发/分布式编程语言现有理论的需求。因此，我们把重点放在并发/分布式编程语言的理论研究比我们最初的计划。因此，虽然我们还没有完成分布式编程语言的实现，但我们在分布式编程语言的理论基础上获得了新的，良好的结果。结果总结如下。分析并发/分布式程序行为的类型系统为了保证并发/分布式程序的正确性，我们开发了静态类型系统及其分析死锁、活锁、竞争条件等的类型检查/重构算法，这些类型系统可以保证， 关于我们 例如，某些通信最终成功，没有两个进程同时进入临界区。基于这些类型系统，我们实现了一个进程演算的分析器，称为π演算。计算模型是分布式程序设计语言的基础我们用表示位置的模态算子扩展了吉拉德的线性逻辑，并在此基础上构造了一个分布式计算模型，在这个模型中，分布式过程用扩展线性逻辑的公式表示，分布式计算对应于逻辑中的演绎。我们证明了计算模型可以优雅地为分布式计算的基本机制（如迁移和位置依赖性）建模。面向对象编程的高级特性的形式化我们形式化了编程语言Java及其扩展的高级特性，例如参数类和内部类。特别是，我们展示了如何将这些功能编译成一个更小的核心语言，并证明了编译的正确性。少

The initial aim of this research project was to design and implement distributed programming languages based on advanced theoretical foundations for concurrent/distributed computation. While conducting this reseach, we faced with needs for further extending existing theories for concurrent/distributed programming languages. Theorefore, we put a more emphasis on theoretical studies for concurrent/distributed programming languages than we initially planned. As a result, although we have not finished implementation of a distributed programming language, we obtained new, good results on theoretical foundations for distributed programming languages. The results are summarized as follows.- Type sytems for analyzing the behavior of concurrent/distributed programsTo guarantee the correctness of concurrent/distributed programs, we developed static type systems and their type check/reconstruction algorithms for analyzing deadlock, livelock, race conditions, etc. Those type systems can guarantee, … More for example, that certain communications eventually succeed, that no two processes enter critical sections simultaneously. Based on those type systems, we implemented an analyzer for processes of a process calculus called the π-calculus.- Computational model as a basis for distributed programming languagesWe extended Girard's linear logic with modal operators for expressing locations, and constructed a distributed computation model based on it. In this model, distributed processes are expressed by formulas of the extended linear logic, and distributed computation corresponds to deduction in the logic. We showed that the computational model can elegantly model basic mechanisms for distributed computation (such as migration and location-dependency).- Formalization of Advanced Features for Object-Oriented ProgrammingWe formalized advanced features of a programming language Java and its extensions, such as parametric classes and inner classes. In particular, we showed how to compile those features into a smaller, core language, and proves the correctness of the compilation. Less