U.S.-France Cooperative Research (INRIA): Static Types for Reasoning about Concurrent Systems

点击翻译按钮获取中文摘要

This three-year award supports US-France cooperative research in programming languages between Benjamin C. Pierce of Indiana University and Davide Sangiorgi of INRIA (French National Institute for Research in Informatics and Applied Mathematics) at Sophia Antipolis, France. The objective of their research is to study the use of static type information for reasoning about concurrent systems through applications of process calculi. Previous work in this area has shown that systems with subtyping and linearity can be `transplanted` from sequential programming languages to a pure calculus of message-passing concurrency. These refinements have benefits in flexibility and detection of programming errors and can be used to justify useful program equivalences. This work will be extended to investigations on the role of parametric polymorphism and various forms of noninterference between concurrent activities. The US investigator brings to this collaboration expertise in design and implementation of concurrent object-oriented languages and in theoretical studies of type systems. This is complemented by the French investigator's experience in concurrency theory and process calculi.