Paper ID: 5927
Linear Types for Communicating Processes
University of London PhD Thesis
Page Numbers :
URL: This publication is available at this URL.
The use of types is well established in sequential computation,
with a range of benefits which are especially clear in the functional
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
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
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
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.
Keywords: interaction categories, types, concurrent systems, semantics, synchronous programming, specification, verification