There are a couple of languages I'd add to the list:
* Mozart/Oz - will (probably) change your thinking about concurrency.
* Clay - really pushes the idea of generic programming.
* Rust - typestate makes assertions part of the type system.
* Cilk - concurrency again.
BitC was looking quite interesting too, but I haven't heard anything about it for some time now; I hope the project hasn't died off.