[Prev][Next][Index][Thread]

Announce





			GOI and strategies

			Patrick Baillot


We announce the following result: by broadening AJM's definition of
plays and strategies on a LL formula we show that Girard's matrix of
partial functions associated to a proof-net R as defined in [2]
induces a valid history-free strategy on the game F=A1 par ... par An,
where A1,...,An are the conclusions of R. In the case of a proof-net
translated from a PCF- (PCF deprived of the fixed-point operator )
term we obtain the same interpretation as AJM in [1]. This enlightens
the link between AJM's model and the geometry of interaction.

The paper will be prochainly available on FTP at the location
	ftp://ftp.logique.jussieu.fr/pub/scratch/baillot.


[1] S. Abramsky, R. Jagadeesan and P. Malacaria.
Full abstraction for PCF (extend abstract).
Lectures Notes in Computer Science, Sendai,
Japan. Springer-Verlag. (1994), no. 789, 1-15.

[2] J.-Y. Girard.
Geometry of interaction I: an interpretation of system ${F}$.
In Ferro & al., editor, Proceedings of A.S.L. Meetings.
North-Holland, 1988.