Linear type theories, semantics and action calculi

• Main Author: Barber, Andrew G.
• Other Authors: Plotkin, Gordon. : Gardner, Phillipa
• Published: University of Edinburgh 1997
• Subjects: 005.101
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561689

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.