Papers related to this topic can be found on Jim Caldwell's home page under papers .

Also, don't miss the lecture notes describing an extension of G\"odels system T, the Curry-Howard Isomorphism, and Proofs as Programs. These notes are from a course given by Bob Constable at Cornell in the Fall 1992 semester. This note presents a set of proof rules for the logic side of the interpretation side-by-side with the typing rules.