UNIVERSITY of GLASGOW

Computing at Glasgow University
 
Paper ID: 6964
DCS Tech Report Number:

Session Types for Inter-Process Communication
Gay,S.J. Vasconcelos,V.T. Ravara,A.

Publication Type: Tech Report (internal)
Appeared in: DCS Tech Report
Page Numbers :
Publisher: Dept of Computing Science, University of Glasgow
Year: 2003
Abstract:

We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies not only the data types of individual messages, but also the state transitions of a protocol and hence the allowable sequences of messages. Although session types are well understood in the context of the pi-calculus, our formulation is based on lambda-calculus with side-effecting input/output operations and is different in significant ways. Our typing judgements statically describe dynamic changes in the types of channels, our channel types statically track aliasing, and our function types not only specify argument and result types but also describe changes in channel types. After formalising the syntax, semantics and typing rules of our language, and proving a subject reduction theorem, we outline some possibilities for extending this work to a concurrent object-oriented language.

Keywords: Session types, static typechecking, semantics, distributedprogramming, specification of communication protocols


PDF Bibtex entry Endnote XML