I was recommended that paper by someone else. Just need to get around to reading it :) The main roadblock I'm having right now is typechecking. I've implemente

I was recommended that paper by someone else. Just need to get around to reading it :) The main roadblock I'm having right now is typechecking. I've implemented Hindley Milner in Haskell and played around with Turnstile, but I still don't know enough theory to invent my own type rules for an imperative language. Something like "Type Theory for the Working Programmer" would be excellent. I just got a copy of TaPL, so maybe I'll just use that.