Title
Type checking choreography description language
Abstract
The Web Services Choreography Description Language (WS-CDL) is a W3C specification developed for the description of peer-to-peer collaborations of participants from a global viewpoint. Currently WS-CDL has no rigorous static type checking. We believe that introducing a type system will exclude many design and description errors, and ensure desirable properties of the choreography specifications. In this paper, we took a core language CDL, which covers most of the important features of the WS-CDL, and is more convenient for the study. We developed the abstract syntax and operational semantics of CDL, and defined a collection of rules which can be used to check if choreography is well-typed. Moreover, we also proved some type safety theorems for CDL in the sense that well-typed choreography cannot get stuck. We show how the use of type information can allow us to gain confidence in the correctness of choreography.
Year
DOI
Venue
2006
10.1007/11901433_15
ICFEM
Keywords
Field
DocType
type system,type safety,abstract syntax,operational semantics,choreography,web service
Operational semantics,Programming language,Type checking,Computer science,Correctness,Choreography,Abstract syntax,Core language,Type safety
Conference
Volume
Issue
ISSN
4260 LNCS
null
0302-9743
ISBN
Citations 
PageRank 
3-540-47460-9
11
0.87
References 
Authors
8
5
Name
Order
Citations
PageRank
Hongli Yang119114.80
Xiangpeng Zhao235320.67
Zongyan Qiu343641.04
Chao Cai41458.48
Geguang Pu560257.89