Brigitte Pientka. Programming Inductive Proofs - A New Approach Based on Contextual Types. In Simon Siegler, Nathan Wasser, editors, Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday. Volume 6463 of Lecture Notes in Computer Science, pages 1-16, Springer, 2010. [doi]