<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>5778</REFNUM><AUTHORS><AUTHOR>Abramsky,S.</AUTHOR><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Nagarajan,R.</AUTHOR></AUTHORS><YEAR>1996</YEAR><TITLE>Specification Structures and Propositions-as-Types for Concurrency</TITLE><PLACE_PUBLISHED>Logics for Concurrency: Structure vs. Automata. - Proceedings of the VIIIth Banff Higher Order Workshop (Birtwistle, G. and Moller, F., Eds.). Lecture Notes in Computer Science, Volume No 1043 DOI: 10.1007/3-540-60915-6_2</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><PAGES>5-40</PAGES><ISBN>3-540-60915-6</ISBN><LABEL>Abramsky:1996:5778</LABEL><KEYWORDS><KEYWORD>specification</KEYWORD></KEYWORDS<ABSTRACT>Many different notions of "property of interest" and methods of verifying such properties arise naturally in programming. A general framework of "Specification Structures" is presented for combining different notions and methods in a coherent fashion. This is then applied to concurrency in the setting of Interaction Categories. As an example, we present a type system for concurrent processes strong enough to guarantee deadlock-freedom, and expressive enough to allow the treatment of some standard examples from the literature. This is illustrated using the classic Dining Philosophers problem.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/banff.pdf</URL></RECORD></RECORDS></XML>