*Abstract:*

In this thesis, we study linear type-theories and their semantics. We present a general framework for such type-theories, and prove certain decidability properties of its equality. We also present intuitionistic linear logic and Milner's action calculi as instances of the framework, and use our results to show decidability of their respective equality judgements.

Firstly, we motivate our development by giving a split-context
logic and type-theory, called *dual intuitionistic linear
logic* (DILL), which is
equivalent at the level of term equality to the familiar
type-theory derived from intuitionistic linear logic (ILL). We give a semantics for the type-theory
DILL, and prove soundness and
completeness for it; we can then deduce these results for the
type-theory ILL by virtue of our
translation.

Secondly, we generalise DILL to
obtain a general logic, type-theory and semantics based on an
arbitrary set of *operators*, or general natural deduction
rules. We again prove soundness and completeness results, augmented
in this case by an initiality result. We introduce Milner's
*action calculi*, and present example instances of our
framework which are isomorphic to them. We extend this isomorphism
to three significant *higher-order* variants of the action
calculi, having functional properties, and compare the induced
semantics for these action calculi with those given previously.

Thirdly, motivated by these functional extensions, we define
*higher-order* instances of our general framework, which are
equipped with functional structure, proceeding as before to give
logic, type-theory and semantics. We show that the logic and
type-theory DILL arise as a
higher-order instance of our general framework. We then define the
*higher-order extension* of any instance of our framework,
and use a Yoneda lemma argument to show that the obvious embedding
from an instance into its higher-order extension is conservative.
This has the corollary that the embeddings from the action calculi
into the higher-order action calculi are all conservative,
extending a result of Milner.

Finally, we introduce relations, a syntax derived from proof-nets, for our general framework, and use them to show that certain instances of our framework, including some higher-order instances, have decidable equality judgements. This immediately shows that the equalities of DILL, ILL, the action calculi and the higher-order action calculi are decidable.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file