Technical Report Available

The following technical report is available from:


Types for Correct Communication in Client-Server Systems

Simon Gay, Department of Computing Science, University of Glasgow

Malcolm Hole, Department of Computer Science, Royal Holloway,
University of London

We define an extension of the pi-calculus which supports extended
patterns of communication, such as client-server protocols. We then
present a static type system for the language which allows concise
high-level specifications of these protocols. The channels on which
the constituent communications of these protocols take place are given
linear types. This allows us to guarantee that a protocol will not
fail to complete due to the pattern of communication between client
and server being incompatible. We use the POP3 protocol as a concrete
example of this technique. Finally, we discuss our plans to add
subtyping to the system and to implement the type system as an
addition to the Pict programming language.