The Fine Structure of Game Lambda Models

Pietro Di Gianantonio Gianluca Franco

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


We study models of the untyped lambda calculus in the setting of game semantics. In particular, we show that, in the category of games introduced by Abramsky, Jagadeesan and Malacaria, all lambda models can be partitioned in three disjoint classes, and each model in a class induces the same theory, i.e. the set of equations between terms. These are the theory H*, the theory which identifies two terms if and only if they have the same Boehm tree and the theory which identifies all the terms which have the same Levy-Longo tree.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Start Conference Manager
Conference Systems