[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Dear Types, while we have many possible types for \omega in Curry-style System F (or \lambda 2, as by Barendregt): is there any publication that contains a reasonably formal “direct" argument/proof why \Omega = \omega\omega is _not_ Curry-typable in System F? I mean “direct” in the sense of not indirectly arguing with the strong normalization theorem. The closest I could find is in the book “Type Theory and Formal Proof” by Nederpelt and Geuvers just telling that it would be “far from obvious” (p 81) ... == Uwe ==
