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. As an example of using Russell to develop programs with dependent types, I implemented the Finger Tree data structure [3] in Coq. It gives quite a few insights about the power of dependent types for specification and their practical use [4]. 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 [5] 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.