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

基于并发/分布式计算先进理论的分布式编程语言的实现

• 批准号: 10558040
• 负责人: KOBAYASHI Naoki
• 金额: $ 3.14万
• 依托单位: Tokyo Institute of Technology (2000)The University of Tokyo (1998-1999)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (B).
• 财政年份: 1998
• 资助国家: 日本
• 起止时间: 1998 至 2000
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-10558040/
• 关键词: distributed programming; concurrency; type systems; program analysis; deadlock; process calculus; linear logic; object-oriented programming; 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

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

项目成果

A.Igarashi,B.C.Pierce,and P.Wadler: "Featherweight Java : A Minimal Core Calculus for Java and GJ"ACM SIGPLAN Notices (Proc.OOPSLA'99). 34(10). 132-146 (1999)

A.Igarashi、B.C.Pierce 和 P.Wadler：“Featherweight Java：Java 和 GJ 的最小核心微积分”ACM SIGPLAN 通知 (Proc.OOPSLA99)。

Eijiro Sumii and Naoki Kobayashi: "A Generalized Deadlock-Free Process Calculus" Proceedings of Workshop on High-Level Concurrent Language (HLCL'98),Electronic Notes on Theoretical Computer Science,Elsvier publishers. 16-3. 55-77 (1998)

Eijiro Sumii 和 Naoki Kobayashi：“广义无死锁过程微积分”高级并发语言研讨会论文集 (HLCL98)，理论计算机科学电子笔记，爱思唯尔出版社。

N.Kobayashi,B.C.Pierce,and D.N.Turner: "Linearity and the Pi-Calculus"ACM Transactions on Programming Langauges and Systems. 21(5). 914-947 (1999)

N.Kobayashi、B.C.Pierce 和 D.N.Turner：“线性和 Pi 微积分”ACM 编程语言和系统汇刊。

Naoki Kobayashi: "Type Systems for Concurrent Processes : From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness"Proceedings of IFIP TCS2000, Springer LNCS. 1872. 365-389 (2000)

Naoki Kobayashi：“并发进程的类型系统：从无死锁到无活锁、时间限制”IFIP TCS2000 论文集，Springer LNCS。

A.Igarashi and B.C.Pierce: "On Inner Classes"Information and Computation. (印刷中). (2000)

A.Igarashi 和 B.C.Pierce：“论内部类”信息和计算（印刷中）。