<XML><RECORDS><RECORD><REFERENCE_TYPE>31</REFERENCE_TYPE><REFNUM>5927</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR></AUTHORS><YEAR>1995</YEAR><TITLE>Linear Types for Communicating Processes</TITLE><PLACE_PUBLISHED>University of London PhD Thesis</PLACE_PUBLISHED><PUBLISHER>N/A</PUBLISHER><LABEL>Gay:1995:5927</LABEL><KEYWORDS><KEYWORD>interaction categories</KEYWORD></KEYWORDS<ABSTRACT>The use of types is well established in sequential computation, with a range of benefits which are especially clear in the functional programming paradigm. o Types are specifications of simple correctness properties, which can be automatically verified by a compiler. o The Curry-Howard isomorphism provides elegant connections with intuitionistic logic. o The categorical semantics of a language can be naturally structured by its type system. Abramsky's theory of interaction categories provides a framework for the transfer of these benefits to concurrency. This thesis is a study of the foundations and applications of that theory. o The fundamental examples of interaction categories are defined: the category SProc of synchronous processes and the category ASProc of asynchronous processes. An abstract axiomatisation of interaction categories is proposed, based on the essential features of these examples. o The use of SProc as a semantic category of processes is illustrated by defining a semantics of dataflow. This is shown to agree with the classical Kahn semantics, and is applied to the language Lustre. o New categories are defined in which the types are powerful enough to guarantee deadlock-freedom of processes satisfying them, so that type-checking methods can be used to support compositional reasoning about deadlock-freedom. This idea is applied to both synchronous and asynchronous examples. o A calculus of synchronous processes is defined, with a type system based on the structure of interaction categories; this corresponds to classical linear logic under the Curry-Howard isomorphism. The calculus has a denotational semantics in any category with suitable structure, which is specified abstractly, and an operational semantics which matches the categorical semantics when SProc is taken as the semantic category.</ABSTRACT><URL>http://www.dcs.gla.ac.uk/~simon/publications/thesis.pdf</URL></RECORD></RECORDS></XML>