[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> Is there a denotational semantics for System Fω in literature > that supports both recursive types and general recursion? Domain-theoreic models with a "type of all types" support these features and also some form of dependent types. R. Amadio, K.B. Bruce, G. Longo The finitary projection model for second order lambda calculus and solutions to higher order domain equations A. Meyer (Ed.), Logic in Computer Science, IEEE Computer Soc, Washington, DC (1986), pp. 122–130 Another model where types are "closures" on a universal domain can be found in N. McCracken An Investigation of a Programming Language with a Polymorphic Type Structure Doctoral dissertation, Syracuse University (1979) More domain-theoretic models can be found in Thierry Coquand, Carl Gunter, Glynn Winskel, Domain theoretic models of polymorphism, Information and Computation, Volume 81, Issue 2, 1989, Pages 123-167 Best Regards Eugenio Moggi
