Type checking a multithreaded functional language with session types

  • Ravara A
  • Vasconcelos V
  • Gay S
Citations of this article
Mendeley users who have this article in their library.
Get full text


We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static type checking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus type checking can verify both correctness of individual messages and correctness of sequences of transitions. Previously, session types have mainly been studied in the context of the @p-calculus; instead, our formulation is based on a multithreaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and type checking system of our language, and prove subject reduction and runtime type safety theorems.




Ravara, A., Vasconcelos, V., & Gay, S. J. (2006). Type checking a multithreaded functional language with session types. Theoretical Computer Science, 368(1–2), 64–87. https://doi.org/10.1016/j.tcs.2006.06.028

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free