Introduction The general goal of our research group is to design and implement programming languages based on solid theoretical foundations. Our particular interests are currently in concurrent/parallel programming languages: in spite of the difficulty of writing and debugging concurrent/parallel programs, little support for them has been provided by concurrent programming languages. Following many successes of theoretical foundations in sequential programming languages (such as lambda-calculus in functional languages), we are trying to establish good principles for design and implementation of concurrent programming languages. We have so far designed and implemented a concurrent programming language HACL and a parallel constraint logic programming language PARCS ; and we studied several type systems, program analyses, and compilation techniques for those languages. Recent Research Topics ( papers )
We are currently studying two schemes for static memory management (or, compile-time garbage collection): linear types and region inference. Linear type systems guarantee that certain values are used just once at run-time; so, such values can be deallocated immediately after being used, without help of conventional garbage collection. Actually, however, not so many values are judged to be linear by traditional linear type systems, hence their applications have been rather limited. In order to overcome this limitation, we developed a new variant of linear type system, called a quasi-linear type system. More information is available here. In parallel to the development of the quasi-linear type system, we have been working on integration of region-based memory management with conventional garbage collection. The main difficulty was that the region-based memory management may create dangling pointers. We overcame it by using region/type information at garbage collection time. On this topic, only a paper written in Japanese is available right now.
Basic computation models are important for good design and implementation of programming languages. We have proposed a concurrent linear logic programming framework called HACL, based on the view ``computation = controlled deduction in linear logic.'' HACL is a rather low level model for concurrent computation, but it has been shown that it can also serve as a basis for higher-level computation models like concurrent object-oriented computation; therefore, HACL can be used as a common basis for studying types systems, program analyses, and implementation techniques of concurrent programming languages. A concurrent programming language HACL was designed and implemented based on the framework. It can be considered an ML extended with primitives for parallel execution, dynamic creation of first-class communication channels, and asynchronous communication over those channels.
While communication is one of the most basic features in concurrent programming languages, it is also one of the major sources of bugs and inefficiency of concurrent programs. Our linear type system can improve the safety and efficiency of concurrent programs, by ensuring that certain channels (called linear channels) are used just once. A linear channel can be reclaimed as soon as the communication takes place, reducing memory management overhead particularly in distributed environments. Furthermore, the linearity enables aggressive compiler optimizations (e.g., forwarder elimination, which is a parallel analogue of tail call elimination). A process equivalence theory based on the linear type system has been developed to show the validity of the compiler optimizations. A type inference algorithm has also been developed. We are now incorporating the type inference and optimizations into the compiler of HACL.
Deadlock and non-determinism are major sources for the difficulty of writing and debugging concurrent programs. They also make static decision of control flows difficult, disabling efficient implementation. We developed a novel static type system that can ensure partial deadlock-freedom and determinacy. In that type system, channels are classified into reliable and unreliable channels: it is statically ensured that reliable channels never cause deadlock and that certain reliable channels never cause non-determinism. Parallel function primitives can be, for example, implemented in the deadlock and deterministic fragment, and many concurrent objects are ensured to be deadlock-free by the type system.
Types have been playing a great role in many advanced compilation techniques for modern sequential programming languages. We have shown that types are also very useful for implementation of concurrent programming languages, particularly for optimizations of communication. The proposed technique enables (almost) tag-free communication of high-level data in distributed environments. It has been incorporated in the distributed implementation of HACL.