"A predicative analysis of structural recursion."

Andreas Abel, Thorsten Altenkirch (2002)
a service of Schloss Dagstuhl - Leibniz Center for Informatics