Adapting Proofs-as-Programs - Poernomo, Iman Hafiz; Crossley, John N.; Gries, David; Schneider, Fred B.; Wirsing, Martin (Springer New York, 2005)