Re: [TYPES] typability in Curry-style System F

Paweł Urzyczyn <urzy-Q8V+/[email protected]> Tue, 9 Feb 2021 11:38:18 +0100

Newsgroups	gmane.comp.science.types
Message-ID	<[email protected]>

[ 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