<XML><RECORDS><RECORD><REFERENCE_TYPE>7</REFERENCE_TYPE><REFNUM>5923</REFNUM><AUTHORS><AUTHOR>Abramsky,S.</AUTHOR><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Nagarajan,R.</AUTHOR></AUTHORS><YEAR>1996</YEAR><TITLE>Interaction Categories and the Foundations of Typed Concurrent Programming</TITLE><PLACE_PUBLISHED>Deductive Program Design: Proceedings of the 1994 Marktoberdorf Summer School (M. Broy, ed.). NATO ASI Series F, Springer-Verlag</PLACE_PUBLISHED><PUBLISHER>Springer</PUBLISHER><LABEL>Abramsky:1996:5923</LABEL><KEYWORDS><KEYWORD>interaction categories</KEYWORD></KEYWORDS<ABSTRACT>We propose Interaction Categories as a new paradigm for the semantics of functional and concurrent computation. Interaction categories have specifications as objects, processes as morphisms, and interaction as composition. We introduce two key examples of interaction categories for concurrent computation and indicate how a geeneral axiomatisation can be developed. The upshot of our approach is that tradiational process calculus is reconstituted in functorial form, and integrated with type theory and functional programming. A second contribution of the paper is to propose a way of combining the Propositions-as-Types and Verification paradigms based on the notion of Specification Structure. We describe specification structures for liveness properties and deadlock-freedom, and illustrate our ideas using a standard example from concurrency theory.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/mdorf.pdf</URL></RECORD></RECORDS></XML>