Xavier Leroy. Well-founded recursion done right. In CoqPL 2024: The Tenth International Workshop on Coq for Programming Languages, London, United Kingdom, January 2024. ACM.

Several Coq libraries and extensions support the definition of non-structural recursive functions using well-founded orderings for termination. After pointing out some drawbacks of these existing approaches, we advocate going back to the basics and defining recursive functions by explicit structural induction on a proof of accessibility of the principal recursive argument.

bib | At HAL | Local copy ] Back

This file was generated by bibtex2html 1.99.