Coq the most successful implementation of a dependent type theory. Serves both as a programming language and a proof assistant. Coq is a central object in my research.
Melt an Ocaml library and preprocessor to generate Latex documents. It saved me countless hours and immense frustration. It is still a little too much tailored to the needs of the few contributors, and development is going slowly. But you may still consider using it.