Programming with Dependent Types

Wouter Swierstra, João Paulo Pizani Flor, and Victor Cacciari Miraldo

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 to datatype generic programming.