Dependent types linkdump

This dependent typing thing has me. For the first time in years I find I'm actually learning something about programming. There is life after the Observer pattern.

Here's a list of some papers I've found worthwhile or just found, and not read yet...

Fun with Type Functions (slides). Oleg Kiselyov, Simon Peyton Jones, Chung-chieh Shan. 2010.

How to fake it with Haskell's recently added type families. But Haskell increasingly looks horribly impure: it's not just that every type's inhabited by bottom, type-level programming is untyped! I think they really should work on their purity! ;) Mentions Ωmega's kind system - my prediction: typed type-level programming is coming to Haskell soon.

Proof-assistants using dependent type systems. Henk Barendregt, Herman Geuvers. 2001.

Recommended as a great intro to all things dependent typing. Not by me though, as I still have to read it.

ΠΣ: Dependent Types without the Sugar. Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, Nicolas Oury. 2009ish.

What's under the sugary hood of dependent programming languages. For when I develop a dependent language - because I'll have to.

A Tutorial Implementation of a Dependently Typed Lambda Calculus. Andres Löh, Conor McBride and Wouter Swierstra. 2009.

Also frequently mentioned as an intro to dependent types.

Verified Programming in GURU. Aaron Stump. 2009.

A book on dependent programming with a focus on verification.

Generic Programming with Dependent Types (part II, part III). Stephanie Weirich. 2010.

Slides focussing on the extra expressivity afforded by dependent types. Agda.

An Epigram Implementation. Edwin Brady, James Chapman, Pierre-Evariste Dagand, Adam Gundry, Conor McBride, Peter Morris, Ulf Norell, Nicolas Oury. 2010.

The 300-page literate Epigram (2?) implementation.