[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
W dniu 08.02.2021 o 19:56, Uwe Nestmann pisze:
is there any publication that contains a reasonably formal “direct" argument/proof why \Omega = \omega\omega is_not_ Curry-typable in System F?
------------- Dear Uwe, this is Exercise 11.16 in Sorensen-Urzyczyn: Lectures on the Curry-Howard Isomorphism. Best regards, Paweł Urzyczyn
