By way of a link to a Lambda-the-Ultimate post from Nathan, here’s an interesting paper that attempts to avoid some paradox of Frege’s.

This paper claims that you can allow unrestricted impredicative quantification if you keep careful track of Frege’s sense-reference distinction, and distinguish between predicates and names of predicates. This (if it really works — I haven’t done more than skim the paper yet) would be a different method of using a predicative hierarchy to avoid the paradoxes.

Paul C. Gilmore’s An Intentional Type Theory: Motivation and Cut-Elimination

Disclaimer: I haven’t yet had the time to read the paper, so by “interesting”, I mean that I’m interested in looking at it myself :-P Mostly, this post was to serve as a later reminder for me to read it! And yes, I will indeed post comments & observations when I get around to it.