Papers related to this topic can be found on Jim Caldwell's home page under
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.