Lambda the Ultimate

My current work deals with extracting security properties from C source code. Without entering too much into the details, it started as a type-and-effects type system with dependent types, but it's slowly starting to look like abstract interpretation-and-effects. Now, my knowledge of abstract interpretation is somewhat limited: I have read one or two of Girard's papers, and everything else I know comes from talks and discussions. So I guess it's time for me to learn more.

So, here's the question: does anyone around here have good references on abstract interpretation and the techniques involved?