Type systems are undecidable more often than not — even in relatively simple cases like Java. A collection of papers.