Shen is an example of a language with a richer type system. Dependent types can be implementated in Shen.
Dependent types correspond to first-order logic in the Curry-Howard interpretation. I don't know much of anything about Shen, so I can't comment further on it specifically.
By the way, limited dependent types can also be implemented in Haskell through type-level programming. The paper that introduced this idea [0] is a good read, and doing some type-level programming is a great way to get to grips with the ins and outs of Haskell's type system. If you're interested in type-level hackery, also be sure to read the HList paper [1].
0. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.2...
http://www.cs.uu.nl/education/scripties/pdf.php?SID=INF/SCR-...
There's also typed racket, which i don't know anything, it's been mentioned to me as "theorems for free"