Leading edge language type system research: Cayenne and Epigram (links)
Cayenne (programming language) is implemented in Haskell and provides a very rich research alternative with dependent types Epigram (programming language) is based on ALF , and for which the compiler can certify a proof of correctness thanks to the strong type system also based on dependent types At first, those listed weren't of an interest to me, but the more I browse through their materials, the more I'm reminded about my goals laid out about an ideal programming environment many years ago. If only these things provided a less ugly syntax... :-)