Multiparty Session Types: Theory and Conversation-Oriented Programming

在工业和社会需求的推动下，通信正迅速成为软件开发的核心要素，如网络服务、业务协议、多核CPU和企业集成。在这种环境中，程序员每个应用程序将有数百个计算节点可供她/他支配，这将在几年内成为一种标准：通信和并发正在成为计算的核心。然而，对于软件如何最好地利用即将到来的环境的力量和丰富性，计算机界、工业界和学术界仍然缺乏成熟的理解。目前在这个问题上缺乏理解-因此没有达成一致-将导致编程、建模、非优化技术以及包括中间件在内的多样化基础设施的开发严重混乱。这个项目旨在帮助开发在编程中利用通信和并发性的一些关键技术元素。该项目的核心是将通信组织为结构化对话的想法，该想法基于该领域最先进的理论之一，多方会话类型，最近由PIS引入。我们对多方会话类型理论进行了推广，并将其应用于著名的面向对象语言Java的扩展设计和实现中，扩展了PIS开发的代码库，所得到的具有多方会话类型的Java语言将用于在两个行业标准ISO Unifi(ISO TC68 WG4 ISO20022 UNIversalFinancial Industry Message SCHEMA)和W3C CDL(ChoreopyDescription Language)中实现现实世界中复杂的金融/商业协议。多党会议类型的理论本身就是由私人投资机构与这些标准的关键人员的对话推动的。通过在已开发的语言、验证器和编译器中实施先进的金融/商业协议，我们不仅可以检查开发的理论相对于实践中发现的一些最复杂的对话模式的实际可用性，而且我们还将使开发的技术想法(包括符号和实现)作为这些标准化努力的一部分可行，而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.