Dependently typed programming is here today: where will it go tomorrow? On the one hand, dependent type theories have grown programming languages; on the other hand, the type systems of programming languages like Haskell (and even C#) are incorporating some kinds of type-level data.

When types involve data, they can capture relationships between data, internalising invariants necessary for appropriate computation. When data describe types, we can express patterns of programming in code. We're beginning to see how to take advantage of the power and precision which dependent types afford, but there are still plenty of problems to address and issues to resolve. The design space is large: this workshop is a forum for researchers who are exploring it.

We hope that the workshop will attract people who either work on the design and implementation of dependently typed programming languages and development environments, or who are using existing systems to develop dependently typed programs or libraries.

This workshop is a sequel to the previous workshops on dependently typed programming in Nottingham in 2008: DTP 2008 and in Edinburgh in 2010: DTP 2010.

Invited speaker

Edwin Brady, University of St Andrews, Systems Programming with Dependent Types


The schedule for DTP 2011 is now online.


You can register through the main ITP website.

Important Dates

Program Committee