06/06/2002: Furio Honsell (Univ. Udine)
Informal seminar on models of lambda-calculi

Résumé

We shall present various results and open questions on the F-completeness of various classes af models of untyped lambda-calculus.
We recall that if M' included in M are two classes of lambda-models, and F is a class of formulae, M' is F-complete w.r.t. M if, for every formula Phi in F, whenever all the models in M' satisfy Phi, all the models in M satisfy Phi too.
If time permits, we shall present some elementary uses of pre-logical relations to models of polymorphism. öaut;