notes-computer-programming-programmingLanguageDesign-prosAndCons-dependentTypes

Why Dependent Types Matter: http://www.cs.nott.ac.uk/%7Etxa/publ/ydtm.pdf

increase expressiveness:

http://www.seas.upenn.edu/%7Esweirich/ssgip/main.pdf