Session types for inter-process communication

We define a language whose type system allows complex protocols to be specified by types. Our formulation is based on the lambda-calculus with side-effecting input/output operations, where typing judgements describe dynamic changes in the type of channels, channel types track aliasing, and function types describe changes in channel types.