| Project/Area Number |
10558040
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B).
|
| Allocation Type | Single-year Grants |
|---|
| Section | 展開研究 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Tokyo Institute of Technology (2000)
The University of Tokyo (1998-1999) |
|---|
Principal Investigator |
KOBAYASHI Naoki Tokyo Institute of Technology, Graduate School of Information Science and Engineering, Assoc. Prof., 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TONOUCHI Toshio NEC Co., Computer & Comm. Media Reseach, Assist. Manager, 情報メディア通信研究本部, 主任(研究職)
IGARASHI Atsushi University of Tokyo, Graduate School of Arts and Sciences, Research Assoc, 大学院・総合文化研究科, 助手 (40323456)
YONEZAWA Akinori University of Tokyo, Graduate School of Science, Prof., 大学院・理学系研究科, 教授 (00133116)
|
|---|
| Project Period (FY) |
1998 – 2000
|
| Project Status |
Completed (Fiscal Year 2000)
|
| Budget Amount *help |
¥4,900,000 (Direct Cost: ¥4,900,000)
Fiscal Year 2000: ¥1,200,000 (Direct Cost: ¥1,200,000)
Fiscal Year 1999: ¥1,400,000 (Direct Cost: ¥1,400,000)
Fiscal Year 1998: ¥2,300,000 (Direct Cost: ¥2,300,000)
|
|---|
| Keywords | distributed programming / concurrency / type systems / program analysis / deadlock / process calculus / linear logic / object-oriented programming / Java / 型推論 / 部分評価 |
|---|
| Research Abstract |
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 programs
To 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 languages
We 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 Programming
We 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
|
