Research directions

Abramsky has developed a concurrent version of game semantics, using the Kahn-Plotkin theory of concrete domains and sequential functions. This has been used to give a game semantics for Classical Linear Logic. It has also been used to give a model for logic with branching quantifiers and information hiding, as proposed by Hintikka. This work was presented in invited talks given at the Workshop on ``Problems and Advance in the Semantics of Linear Logic'' held in Utrecht, November 28th and 29th 1997, and at the Amsterdam Colloquium, December 17-20 1997. Honda and Yoshida developed a version of game semantics for call-by-value PCF, and proved a full abstraction result. Their description of their model used some tools from the pi-calculus. Abramsky and McCusker gave a more abstract and general construction of call-by-value models from call-by-name ones, and showed that when applied to the call-by-name games model of PCF it gave rise to the call-by-value one of Honda and Yoshida; when applied to the model for the richer functional language FPC studied by McCusker in his thesis, it gave a fully abstract model for call-by-value FPC; and when applied to the model previously given by them for Idealized Algol, it gave a full abstract model for a fragment of ML with ground reference types.

Honda and Yoshida's paper appeared in ICALP `97, while Abramsky and McCusker's paper was given in CSL `97, and will appear in the proceedings of that conference. Subsequently, Abramsky, Honda and McCusker have obtained a fully abstract games model for general reference types; a paper containing this result has been submitted to LiCS `98.

A factorisation theorem in the sense of Freyd & Kelly has been obtained by Melliès in the framework of axiomatic rewriting systems. The theorem means that the efficient part of a computation can always be separated from its useless part modulo redex permutations, and that this separation is categorically functorial. This work was presented at the Confer workshop in Bologna and at the CTCS `97 conference in Santa Margherita.

Subsequently, Melliès has obtained a stability result in the sense of Berry expressing the existence of a cone $(e_i:M\to V_i)_{i\in I}$ of minimal computations from any term M to the set of its values V_i. The result whose proof relies heavily on the factorisation theorem is verified by any axiomatic rewriting system. In the lambda-calculus, it extends the result by Wadsworth that the head-reduction is the minimal reduction path from a lambda-term to its head-normal form. In the call-by-value lambda-calculus, the cone $(e_i:M\to V_i)_{i\in I}$ contains at most a singleton which describes the strategy of Landin SECD machine. In the lambda-sigma calculus, the existence of a cone and its finiteness implies the completeness of various weak strategies and the corresponding abstract machines. A paper containing these results has been submitted to LiCS `98.