gistfile1.txt

There are a lot of resources to learn from, and it's hard to pick just one. Below are links to learning about dependently typed programming. I think that the most comfortable path is to learn DT programming first, and then learn more of the pure math and type theory behind it along the way as you get more experienced.

Basically, Coq is the most mature and oldest, but is more tedious to do dependently typed programming with.
Agda is not as mature, but it supports dependently typed programming very well.
Idris is an even newer language that also supports dependently typed programming well, and IMO has the best chance of being a practically used language.
Personally, I mostly use Agda.

Coq:
Software foundations - http://www.cis.upenn.edu/~bcpierce/sf/toc.html
Certified programming with dependent types - http://adam.chlipala.net/cpdt/

Agda:
Dependently typed programming in Agda (Agda tutorial) - http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
The power of pi - http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.175.8947&rep=rep1&type=pdf

Idris:
Idris tutorial - http://docs.idris-lang.org/en/latest/tutorial/index.html#tutorial-index
Idris course (4 videos and slides) - http://edwinb.wordpress.com/2013/03/15/idris-course-at-itu-slides-and-video/