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

这个为期三年的奖项支持美国和法国在编程方面的合作研究 本杰明·C.印第安纳州大学的皮尔斯和 法国国家信息学和应用数学研究所 索菲亚·安提波利斯，法国 他们研究的目的是研究静态 通过进程应用推理并发系统的类型信息 结石 这一领域以前的工作表明，具有子类型和线性的系统 可以从顺序编程语言“移植”到纯微积分中， 消息传递并发性。 这些改进在灵活性和检测方面都有好处 的编程错误，并可以用来证明有用的程序等效。 这项工作 将扩展到参数多态性的作用和各种调查 同时进行的活动之间互不干涉的形式。 美国调查员为这一合作带来了设计和实施 并发面向对象语言和类型系统的理论研究。 这是 辅以法国研究者在并发理论和过程方面的经验 结石

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.