Multiparty Session Types: Theory and Conversation-Oriented Programming

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

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.