  We refine a model for linear logic based on two well-known ingredients: games
and simulations. We have already shown that usual simulation relations form a
sound notion of morphism between games; and that we can interpret all linear
logic in this way. One particularly interesting point is that we interpret
multiplicative connectives by synchronous operations on games. We refine this
work by giving computational contents to our simulation relations. To achieve
that, we need to restrict to intuitionistic linear logic. This allows to work
in a constructive setting, thus keeping a computational content to the proofs.
We then extend it by showing how to interpret some of the additional structure
of the exponentials. To be more precise, we first give a denotational model for
the typed lambda-calculus; and then give a denotational model for the
differential lambda-calculus of Ehrhard and Regnier. Both this models are
proved correct constructively.
