<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>5151</REFNUM><AUTHORS><AUTHOR>Abramsky,S.</AUTHOR><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Nagarajan,R.</AUTHOR></AUTHORS><YEAR>1997</YEAR><TITLE>A Type-Theoretic Approach to Deadlock-Freedom of Asynchronous Systems</TITLE><PLACE_PUBLISHED>Proceedings of the International Symposium on Theoretical Aspects of Computer Software, TACS'97, Sendai, Japan, (Abadi, M., and Ito, T., Eds.,), Lecture Notes in Computer Science, Volume No. 1281 DOI: 10.1007/BFb0014557</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>295-320</PAGES><ISBN>0302-9743</ISBN><LABEL>Abramsky:1997:5151</LABEL><ABSTRACT>We present a type-based technique for the verification of deadlock-freedom in asynchronous concurrent systems. Our general approach is to start with a simple interaction category, in which objects are types containing safety specifications and morphisms are processes. We then use a specification structure to add information to the types so that they specify stronger properties. In this paper the starting point is the category $\ASProc$ and the extra type information concerns deadlock-freedom. In the resulting category $\ASProcD$, combining well-typed processes preserves deadlock-freedom. It is also possible to accommodate non-compositional methods within the same framework. The systems we consider are asynchronous, hence issues of divergence become significant; our approach incorporates an elegant treatment of both divergence and successful termination. As an example, we use our methods to verify the deadlock-freedom of an implementation of the alternating-bit protocol.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/tacs.pdf</URL></RECORD></RECORDS></XML>