<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>7950</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Hole,M.J.</AUTHOR></AUTHORS><YEAR>2005</YEAR><TITLE>Subtyping for session types in the pi calculus</TITLE><PLACE_PUBLISHED>Acta Informatica 42(2/3) DOI: 10.1007/s00236-005-0177-z</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>191-225</PAGES><ISBN>0001-5903</ISBN><LABEL>Gay:2005:7950</LABEL><KEYWORDS><KEYWORD>pi calclus</KEYWORD></KEYWORDS<ABSTRACT>Extending the pi calculus with the session types proposed by Honda et al. allows high-level specifications of structured patterns of communication, such as client-server protocols, to be expressed as types and verified by static typechecking. We define a notion of subtyping for session types, which allows protocol specifications to be extended in order to describe richer behaviour; for example, an implemented server can be refined without invalidating type-correctness of an overall system. We formalize the syntax, operational semantics and typing rules of an extended pi calculus, prove that typability guarantees absence of run-time communication errors, and show that the typing rules can be transformed into a practical typechecking algorithm.</ABSTRACT></RECORD></RECORDS></XML>