<XML><RECORDS><RECORD><REFERENCE_TYPE>7</REFERENCE_TYPE><REFNUM>5316</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Hankin,C.L.</AUTHOR></AUTHORS><YEAR>1996</YEAR><TITLE>A Program Logic for Gamma</TITLE><PLACE_PUBLISHED>Coordination Programming: Mechanisms, Models and Semantics (J.-M. Andreoli and C. L. Hankin, eds.)</PLACE_PUBLISHED><PUBLISHER>Imperial College Press</PUBLISHER><PAGES>171-194</PAGES><ISBN>1-86094-023-4</ISBN><LABEL>Gay:1996:5316</LABEL><KEYWORDS><KEYWORD>program logic</KEYWORD></KEYWORDS<ABSTRACT>We take a systematic approach to the construction of a program logic for Gamma, by applying Abramsky's domain theory in logical form to a denotational semantics of the language. Starting from a resumption semantics of Gamma, we are able to derive both the formulae and the proof system of the transition assertion logic previously proposed by Errington, Hankin and Jensen. The general theory enables us to prove soundness of the logic, although completeness fails because the resumption semantics of Gamma is not fully abstract. At the end of the paper we discuss the possibilities for obtaining a complete logic.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/coord.pdf</URL></RECORD></RECORDS></XML>