## 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.*