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. This talk is on ongoing joint work with A. Ravara and S. Gay.