Multiparty Session Types: Theory and Conversation-Oriented Programming

在工业和社会需求的推动下，通信正迅速成为软件开发的核心元素，如Web服务、业务协议、多核CPU和企业集成。在这种环境下，程序员将在每个应用程序中拥有数百个计算节点，这将在几年内成为常态：通信和并发性是计算的核心。然而，对于软件如何最好地利用这个即将到来的环境的力量和丰富性的成熟理解，在计算社区，工业界和学术界仍然缺乏。目前在这个问题上缺乏理解-因此缺乏一致-将导致编程、建模、不优化技术以及包括中间件在内的各种基础设施的开发方面的严重混乱。该项目旨在为开发一些关键技术要素做出贡献，以利用编程中的通信和并发能力。该项目的中心思想是将通信组织为结构化对话，基于该领域最先进的理论之一，即最近由PI引入的多方会话类型。我们发展了多方会话类型理论的一个概括，然后将所发展的理论应用于著名的面向对象语言Java的扩展的设计和实现，扩展了也由PI开发的代码库。由此产生的语言，具有多方会话类型的Java，将被用于实现两个行业标准中的真实世界的复杂金融/商业协议，ISO9001（ISO TC 68 WG 4 ISO 20022通用金融行业消息方案）和W3C CDL（编排描述语言）。多方会话类型的理论本身是由PI与这些标准的关键人员的对话激发的。通过在开发的语言、验证器和编译器中实现先进的金融/商业协议，我们不仅可以检查开发的理论相对于实践中发现的一些最复杂的会话模式的实际可用性，而且还可以使用开发的技术思想，包括符号和实现，作为这些标准化工作的一部分，PI一直作为官方邀请成员工作。

Driven by the industrial and social needs, communication is rapidlybecoming the central element of software development, as found in webservices, business protocols, multicore CPUs and corporateintegration. In this environment, a programmer will have hundreds ofcomputing nodes per application at her/his disposal, which will becomea norm in a few years: communication and concurrency is becomingcentral to computing. However a mature understanding on how software can best harness thepower and richness of this coming environment, is still lacking in thecomputing community, industry and academia alike. This current lackof the understanding --- hence lack of agreement --- on this issuewill lead to a dire confusion in programming, in modelling, inoptimisation technologies, and in the development of diverseinfrastructures including middle-ware. This project aims to contributeto the development of some of the key technical elements forharnessing the power of communication and concurrency in programming.The project centres on the idea of organising communication asstructured conversations, based on one of the most advanced theoriesin this area, the multiparty session types, recently introduced by thePIs. We develop a generalisation of the theory of multiparty sessiontypes, then apply the developed theory to a design and implementationof an extension of the well-known object-oriented language, Java,extending the code base which is also developed by the PIs.The resulting language, Java with multiparty session types, will beused to implement real-world complex financial/business protocols inthe two industry standards, ISO UNIFI (ISO TC68 WG4 ISO20022 UNIversalFinancial Industry message scheme) and W3C CDL (ChoreographyDescription Language). The theory of multiparty session types itselfwas motivated by the PIs' dialogue with key personnel of thesestandards. Through implementing advanced financial/business protocolsin the developed language, validator and compiler, not only can weexamine the practical usability of the developed theory vis-a-vis someof the most complex conversation patterns found in practice, but alsowe shall make it viable to use the developed technical ideas includingnotations and implementations as part of these standardisationefforts, for which the PIs have been working as official invitedmembers.