Game Theoretic Analysis of Call-by-value Computation

The following paper is available by anonymous ftp on the site:


Any comments are welcome.

Kohei Honda
Edinburgh University


        Game Theoretic Analysis of Call-by-value Computation

                   Kohei Honda  and  Nobuko Yoshida

                        (Edinburgh University)

                          *** Abstract ***

We introduce a general semantic universe of call-by-value computation
based on elements of game semantics, and validate its appropriateness
as a semantic universe by the full abstraction result for call-by-value
PCF, a generic typed programming language with call-by-value
evaluation. The key idea is to consider the distinction between
call-by-name and call-by-value as that of the structure of information
flow, which determines the basic form of games. In this way the
call-by-name computation and call-by-value computation arise as two
independent instances of sequential functional computation with
distinct algebraic structures. We elucidate the type structures of the
universe following the standard categorical framework developed in the
context of domain theory. Mutual relationship between the presented
category of games and the corresponding call-by-name universe is also