Certified Programming with Dependent Types

[Bernie Pope]

For those of us interested in certified programming and dependent types:

http://adam.chlipala.net/cpdt/

A draft of Adam Chlipala's book on proving programs with Coq.

Cheers,
Bernie.