A programming language's type system provides structure to the values that programs manipulate. This can help catch many simple errors before a program is even run. Programming languages with dependent types enable the programmers to capture even more of the intended meaning of functions and data in their types. Experimental programming languages with dependent types, such as Agda, Coq, Epigram and Idris, offer exciting new opportunities to explore the way types can help us write better programs.
In our group we have applied this technology in the context of various projects, ranging from the design of domain-specific languages (the Pi-Ware project-page) to data type generic programming (PhD Project page).