@InProceedings{	  CastagnaDezaniCiancagliniGiachinoPadovani09,
  author	= {Giuseppe Castagna and Mariangiola Dezani-Ciancaglini and
		  Elena Giachino and Luca Padovani},
  title		= {{F}oundations of {S}ession {T}ypes},
  booktitle	= {Proceedings of the 11th International ACM SIGPLAN
		  Symposium on Principles and Practice of Declarative
		  Programming (PPDP'09)},
  year		= {2009},
  pages		= {219-230},
  publisher	= {ACM},
  url		= {http://www.di.unito.it/~padovani/Papers/FoundationsSessionTypes.pdf}
		  ,
  doi		= {10.1145/1599410.1599437},
  abstract	= {We present a streamlined theory of session types based on
		  a simple yet general and expressive formalism whose main
		  eatures are semantically characterized and where each
		  design choice is semantically justified. We formally define
		  the semantics of session types and use it to devise the
		  subsessioning relation. We give a coinductive
		  characterization of subsessioning and describe algorithms
		  to decide all the key relations defined in the article. We
		  demonstrate the generality and expressive power of our
		  framework by providing a session-based type system for a
		  pi-calculus variant that does not rely on any specialized
		  construct for session-based communication. The type system
		  is shown to guarantee absence of communication errors and
		  global progress.}
}