[Prev][Next][Index][Thread]
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.
Regards,
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
--------------------------------------------------------------------
Title:
Session Types for Inter-Process Communication
Authors:
Simon Gay, Vasco Vasconcelos and Antonio Ravara
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, distributed
programming, specification of communication protocols.