You could take a look at Coquand (2002) “A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions”.

https://www.dropbox.com/s/xmj7yv1i1moe0ag/Coquand2002.pdf

Drop in to #dependent on Freenode IRC, and let’s chat.