文章基本信息

标题：Parameterised Multiparty Session Types
本地全文：下载
作者：Pierre-Malo Denielou ; Nobuko Yoshida ; Andi Bejleri 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2012
卷号：8
期号：4
页码：1
DOI：10.2168/LMCS-8(4:6)2012
出版社：Technical University of Braunschweig
摘要：For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Gödel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.
其他关键词：Session Types, Dependent Types, The Pi-Calculus, G¨odel T, Parallel Algorithms, FFT, Web services.