Technical Report: Session Types for Inter-Process Communication

Dear Types Readers,

We would like to announce the following technical report, which can be
found at http://www.dcs.gla.ac.uk/~simon/publications/TR-2003-133.pdf

Comments are welcome.


Simon Gay

Dr Simon Gay                    Department of Computing Science 
Lecturer in Computing Science   University of Glasgow
                                17 Lilybank Gardens
                                Glasgow G12 8QQ, UK
Phone: +44 141 330 6035
Fax:   +44 141 330 4913
Email: simon@dcs.gla.ac.uk


Session Types for Inter-Process Communication


Simon Gay, Vasco Vasconcelos and Antonio Ravara


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

Session types, static typechecking, semantics, distributed
programming, specification of communication protocols.