[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----] Dear Kim, thank you for the clear statement about the state of the art w.r.t. F_{omega,sub,rec}. It conforms that my understanding wasn't absolutely mistaken. I never doubted that the interesting equations can be solved this way. So I see two possibilities in case one cannot give denotational meaning to the full calculus F_{omega,sub,rec}. Either one just takes it as a metalanguage having suffiicently good operational properties (your choice) or, if one wants to work denotationally based, to consider types a subsets of or pers on some untyped universe. Thomas Streicher 20-Oct-2002 22:37:03 -0300,927;000000000000-00000000