The Little Typer - London Daniel P. Friedman has released The Little Typer - a book introducing dependent types. Paul Cadman has formed a London based type-driven development group where we work through the book.
