<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>5152</REFNUM><AUTHORS><AUTHOR>Abramsky,S.</AUTHOR><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Nagarajan,R.</AUTHOR></AUTHORS><YEAR>1999</YEAR><TITLE>A Specification Structure for Deadlock-Freedom of Synchronous Processes</TITLE><PLACE_PUBLISHED>Theoretical Computer Science 222(1-2) DOI: 10.1016/S0304-3975(98)00189-3</PLACE_PUBLISHED><PUBLISHER>Elsevier Science</PUBLISHER><PAGES>1-53</PAGES><ISBN>0304-3975</ISBN><LABEL>Abramsky:1999:5152</LABEL><KEYWORDS><KEYWORD>deadlock-freedom</KEYWORD></KEYWORDS<ABSTRACT>Many different notions of "program property", and many different methods of verifying such properties, arise naturally in programming. We present a general framework of "Specification Structures" for combining different notions and methods in a coherent fashion. We then apply the idea of specification structures to concurrency in the setting of Interaction Categories. As a specific example, a certain specification structure defined over the interaction category SProc yields a new category SProc_D in which morphisms are deadlock-free concurrent processes and composition is process interaction. SProc_D is obtained from SProc by adding specification information to the objects which is strong enough to guarantee deadlock-freedom. The main technical contribution is to show that this can be done in a way which is preserved by composition. The methods used to achieve this can be seen as a semantic analogue of those used to prove strong normalization in classical linear logic.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/tcs.pdf</URL></RECORD></RECORDS></XML>