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.