Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. FLOPS 2006: 114-129