next up previous contents
Next: Denotational semantics Up: Logics for Concurrency and Previous: Logics for Concurrency and

Game semantics for the $\lambda$-calculus and linear logic

A key interest of game semantics is that it provides a framework within which one may conciliate dynamic and static aspects of meaning. It is expected that such semantics can help in complexity theory on the one hand and in extending denotational semantics to model concurrent and distributed languages (so-called process-calculi).

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. 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.

Danos, Herbelin and Regnier explain, in [DHR96], the operational side of the two game models of Hyland-Ong (HO) and Abramsky-Jagadeesan-Malacaria (AJM) in terms of abstract machines. Building on this explanation, an embedding of the AJM model in the HO model is given that leads to an easy proof of completeness for the former.

In [BDER97], Baillot, Danos, Ehrhard and Regnier adapt the AJM construction to give the first known games model which encompasses all of classical linear logic. Composition of strategies is recast as a communication process. The exponential part of the model is based on the idea of sticking to strategies which contain all possible encodings of copy-tags. This works is pursued in [BDER97b], which gives an explicit transformation that goes from that linear logic games model to the traditional relational model. This concrete extensional collapse helps in understanding what games semantics is good to.

In [CuBoeh] Curien presents a formalism of trees with pointers, called abstract Böhm trees, that provide a suitable abstract framework in which various cut-free proofs or normal terms of several $\lambda$-calculus based languages (including $\mbox{PCF}$ and Parigot's $\lambda\mu$-calculus) can be faithfully encoded. A simple abstract machine allows us to compute over abstract Böhm trees. This machine is closely related to Coquand's interaction sequences and debates. The execution over finite abstract Böhm trees always terminates. We introduce an abstract notion of type that fits the purpose of guaranteeing that the execution cannot go into deadlock, i.e., that it always reaches a satisfactory final state. The operational aspects of (untyped) Böhm trees are investigated in more depth in [CuHer96], a joint paper by Curien and Herbelin,

[[AM97]] S. Abramsky, G. McCusker, Call-by-Value games (extended abstract) To appear in Proc. of CSL'97.

[[BDER97]] P. Baillot, V. Danos, and T. E. andL. Regnier.
Believe it or not, AJM's games model is a model of classical linear logic.
In Proc. 12th LICS, pages 68-75. IEEE, 1997.

[[BDER97b]] P. Baillot, V. Danos, T. Ehrhard, and L. Regnier.
Timeless games.
In Proc. CSL '97, volume to appear. Springer Verlag, 1997.

[[CuBoeh]] P.-L. Curien.
Abstract böhm trees.
Mathematical Structures in Computer Science, 1998.
to appear.

[[CuHer96]] P.-L. Curien and H. Herbelin.
Computing with abstract böhm trees.
In Proc. of Third Fuji International Symposium on Functional and Logic Programming, World Scientific (Singapour), 1998.

[[DHR96]] V. Danos, H. Herbelin, and L. Regnier.
Game semantics and abstract machines.
In Proc. 11th LICS, pages 394-405. IEEE, 1996.

[[HY97]] K. Honda, N. Yoshida, Game-theoretic analysis of Call-by-Value Computation (extended abstract). To appear in Proc. of ICALP'97.


next up previous contents
Next: Denotational semantics Up: Logics for Concurrency and Previous: Logics for Concurrency and

1/10/1998