A thesis submitted to (1996) and accepted by (1997) the University of St Andrews in partial fulfilment of the requirements for the degree of Master of Philosophy.
Supervisor: Dr Roy Dyckhoff (St Andrews)
Examiners: Prof. Ursula Martin (St Andrews), Dr David Pym (London)
Abstract and contents as postscript. (74 Kby)
Forum uses the connectives of linear logic. Languages based on linear logic offer extra expressivity (in comparison with traditional logic languages), but also present new implementation challenges. One such challenge is that of context management, because the multiplicative linear connectives `times', `par' and `lollipop' require context splitting. Hodas and Miller presented a solution (the IO model) to this in 1991 for the language Lolli based on minimal linear logic. This thesis presents a technique which is an adaptation of the aforementioned approach for the language Forum and following a suggestion of Miller that the `?' constant be treated as primitive in order to avoid looping problems arising from its use as a derived symbol. Cervesato, Hodas and Pfenning have presented a technique for managing the `top' constant, dividing each input context into a ``slack'' part and a ``strict'' part; the main novel contribution of this thesis is to modify this technique, by dividing instead the output context. This leads to a proof system with fewer rules (and consequent ease of implementation) but enhanced performance, for which we present some experimental evidence.