I'm trying to write up a blog post about this now. A really good presentation focused on types and programming languages is available in the middle chapters of Practical Foundations for Programming Languages. I originally learned about it from studying Aczel's Antifoundation Axiom from Barwise and Moss' Vicious Circles[0]---in there you can get a much more mathematical foundationalist POV---but Harper's book is more direct.

[0]http://www.amazon.com/Vicious-Circles-Center-Language-Inform...

To provide small insight into the work of people who actually do doubt ZFC I'd like to source two interesting books.

First is Peter Aczel's work with the Anti-foundation Axiom which allows you to create sets with "infinite regress". Instead of blanket disallowing these kinds of set like ZFC does, he enlarges ZFC by allowing any set which is a unique solution to a group of equations that may be self-referential.

I was introduced to this stuff by a book "Vicious Circles" by Barwise and Moss (http://www.amazon.com/Vicious-Circles-Center-Language-Inform...).

The important point is that the Anti-Foundation Axiom lets us model infinite, streaming structures similar to those modeled in computer programs. It also motivates the somewhat unpopular idea of bisimulation which is very necessary for creating a kind of equality in an AFA world... and also for proving the equality of streaming algorithms.

Second is Lawvere's introduction to thinking about the foundations of mathematics from a Category Theoretic perspective. Lawvere is a proponent of thinking of Set theory as simply one, somewhat interesting Category which can be generated by a more foundational theory and set of axioms. I'm not personally anywhere nearly well-knowing enough to say whether that works, but his book Conceptual Mathematics (http://fef.ogu.edu.tr/matbil/eilgaz/kategori.pdf) gives a very interesting POV on how to work from the Category Theoretical basis to answer some normal Set theoretic questions.

Interesting idea, although I find the motivation a little unconvincing. In particular, the quotation

"... natural language abounds with directly or indirectly self-referential yet apparently harmless expressions—all of which are excluded from the Tarskian framework"

used in this article to motivate the concept of inconsistency-tolerant logic is actually much better support for non-well-founded set theories [1] allowing hypersets (i.e. sets which contain themselves), e.g. by assuming Aczel's anti-foundation axiom [2]. Since these set theories are compatible with standard the set theory, extending it, rather than replacing it, they don't throw out the notion of consistency, but have no problem dealing with self-referential sets and such. "Vicious Circles" [3] is a great exposition of the subject of hypersets and their applications to computer science and logic, among other things and is quote accessible for such a theoretical subject.

[1] http://en.wikipedia.org/wiki/Non-well-founded_set_theory

[2] http://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axiom

[3] http://www.amazon.com/Vicious-Circles-Center-Language-Inform...