Galois Tech Talk: Introducing Well-Founded Recursion
Introducing Well-Founded Recursion Eric Mertens
Implementing recursive functions can be tricky when you want to be certain that they eventually terminate. This talk introduces the concept of well-founded recursion as a tool for implementing recursive functions. It implements these concepts in the Agda programming language and demonstrates the technique by implementing a simple version of Quicksort.