Adapting Proofs-as-Programs The Curry-Howard Protocol - Poernomo, Iman Hafiz; Wirsing, Martin; Crossley, John Newsome (Springer New York, 2005)