Re: [TYPES] Fwd: Denotational semantics of Fω with t ype- & term-recursion

[ 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