Coercion par prédicats en Coq. Matthieu Sozeau, Master's Thesis,
Université Paris VII, LRI, Orsay, 2005.
Russell is a language for programming with dependent types in Coq. It uses an adaptation of the predicate subtyping feature of PVS to allow users to write only algorithmic code while using strong specifications. Proof obligations are generated automatically, and, once proved, permit to build a complete, valid Coq term. A report  (in french) with full proofs is available as well as an article  describing the theoretical development. I'm working on a complete formalization of this in Coq, here's the relevant page.
As an example of using Russell to develop programs with dependent types, I implemented the in Coq. It gives quite a few insights about the power of dependent types for specification and their practical use . Here's the relevant page. You can have a look at the example on celebrities in a party inspired by Richard Bird's article. Yet a lighter example: quicksort.
I developed a complete formalization  of simply-typed lambda calculus with constants in the dependently-typed style with the help of Program. It includes a tait-style proof of weak normalization. The Coq file is here.
Here are the slides of a talk i gave at the LRI on Program, Russell's incarnation in Coq. The updated version for another seminar at Gallium.
Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of
Lecture Notes in Computer Science. Springer, 2007, pp.237-252.
Program-ing Finger Trees in Coq in ICFP'07. Matthieu Sozeau. Freiburg, Germany:
ACM Press, 2007, pp.13-24.
ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICFP'07, http://doi.acm.org/10.1145/1291151.1291156
A dependently-typed formalization of simply-typed lambda-calculus: substitution, denotation, normalization. Matthieu Sozeau, Unpublished, 2007 - Literate Coq script.